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

Theorem pm4.71i 632
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 630 . 2
31, 2mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  pm4.24  643  pm4.45  688  anabs1  808  2eu5  2382  imadmrn  5352  dff1o2  5826  f12dfv  6179  xpsnen  7621  dom0  7665  dfac5lem2  8526  pwfseqlem4  9061  axgroth6  9227  eqreznegel  11196  xrnemnf  11357  xrnepnf  11358  elioopnf  11647  elioomnf  11648  elicopnf  11649  elxrge0  11658  isprm2  14225  efgrelexlemb  16768  opsrtoslem1  18148  tgphaus  20615  cfilucfil3OLD  21757  cfilucfil3  21758  ioombl1lem4  21971  vitalilem1  22017  ellogdm  23020  nb3grapr2  24454  is2wlk  24567  0spth  24573  0crct  24626  0cycl  24627  erclwwlkref  24813  erclwwlknref  24825  pjimai  27095  eulerpartlemt0  28308  pm11.58  31296  bnj1101  33843  bj-snglc  34527
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 185  df-an 371
  Copyright terms: Public domain W3C validator