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