Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.71i Unicode version

Theorem pm4.71i 617
 Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)
Hypothesis
Ref Expression
pm4.71i.1
Assertion
Ref Expression
pm4.71i

Proof of Theorem pm4.71i
StepHypRef Expression
1 pm4.71i.1 . 2
2 pm4.71 615 . 2
31, 2mpbi 202 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 178  /\wa 362 This theorem is referenced by:  pm4.24  628  pm4.45  673  anabs1  791  2eu5  2351  imadmrn  5151  dff1o2  5616  map0e  7209  xpsnen  7354  dom0  7398  dfac5lem2  8241  pwfseqlem4  8775  axgroth6  8941  eqreznegel  10885  xrnemnf  11044  xrnepnf  11045  elioopnf  11328  elioomnf  11329  elicopnf  11330  elxrge0  11338  isprm2  13711  efgrelexlemb  16184  opsrtoslem1  17367  tgphaus  19391  cfilucfil3OLD  20529  cfilucfil3  20530  ioombl1lem4  20742  vitalilem1  20788  ellogdm  21825  nb3grapr2  23041  is2wlk  23143  0spth  23149  0crct  23191  0cycl  23192  pjimai  25259  eulerpartlemt0  26455  pm11.58  29316  f12dfv  29820  erclwwlkref  30157  erclwwlknref  30173  bnj1101  31356  bj-snglc  31909 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 179  df-an 364
 Copyright terms: Public domain W3C validator