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  5395  dff1o2  6055  f12dfv  6429  isof1oidb  6474  isof1oopb  6475  xpsnen  7929  dom0  7973  dfac5lem2  8830  pwfseqlem4  9363  axgroth6  9529  eqreznegel  11650  xrnemnf  11827  xrnepnf  11828  elioopnf  12138  elioomnf  12139  elicopnf  12140  elxrge0  12152  isprm2  15233  efgrelexlemb  17986  opsrtoslem1  19305  tgphaus  21730  cfilucfil3  22925  ioombl1lem4  23136  vitalilem1  23182  vitalilem1OLD  23183  ellogdm  24185  nb3grapr2  25983  is2wlk  26095  0spth  26101  0crct  26154  0cycl  26155  erclwwlkref  26341  erclwwlknref  26353  pjimai  28419  dfrp2  28922  eulerpartlemt0  29758  bnj1101  30109  bj-snglc  32150  icorempt2  32375  wl-cases2-dnf  32474  matunitlindf  32577  pm11.58  37612  nb3grpr2  40611  upgr2wlk  40876  erclwwlksref  41241  erclwwlksnref  41253  0spth-av  41294  0Crct  41300  0Cycl  41301
 Copyright terms: Public domain W3C validator