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

Theorem pm4.71i 662
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 660 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))
31, 2mpbi 219 1 (𝜑 ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  pm4.24  673  pm4.45  720  anabs1  846  2eu5  2545  imadmrn  5382  dff1o2  6040  f12dfv  6407  isof1oidb  6452  isof1oopb  6453  xpsnen  7907  dom0  7951  dfac5lem2  8808  pwfseqlem4  9341  axgroth6  9507  eqreznegel  11609  xrnemnf  11791  xrnepnf  11792  elioopnf  12097  elioomnf  12098  elicopnf  12099  elxrge0  12111  isprm2  15182  efgrelexlemb  17935  opsrtoslem1  19254  tgphaus  21678  cfilucfil3  22870  ioombl1lem4  23081  vitalilem1  23127  vitalilem1OLD  23128  ellogdm  24130  nb3grapr2  25777  is2wlk  25889  0spth  25895  0crct  25948  0cycl  25949  erclwwlkref  26135  erclwwlknref  26147  pjimai  28213  dfrp2  28716  eulerpartlemt0  29552  bnj1101  29903  bj-snglc  31944  icorempt2  32169  wl-cases2-dnf  32268  matunitlindf  32371  pm11.58  37406  nb3grpr2  40603  upgr2wlk  40868  erclwwlksref  41233  erclwwlksnref  41245  0spth-av  41286  0Crct  41292  0Cycl  41293
  Copyright terms: Public domain W3C validator