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 665
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 663 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))
31, 2mpbi 220 1 (𝜑 ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 385
This theorem is referenced by:  pm4.24  676  pm4.45  724  anabs1  867  2eu5  2586  rabeqc  3394  imadmrn  5511  dff1o2  6180  f12dfv  6569  isof1oidb  6614  isof1oopb  6615  xpsnen  8085  dom0  8129  dfac5lem2  8985  pwfseqlem4  9522  axgroth6  9688  eqreznegel  11812  xrnemnf  11989  xrnepnf  11990  elioopnf  12305  elioomnf  12306  elicopnf  12307  elxrge0  12319  isprm2  15442  efgrelexlemb  18209  opsrtoslem1  19532  tgphaus  21967  cfilucfil3  23163  ioombl1lem4  23375  vitalilem1  23422  ellogdm  24430  nb3grpr2  26329  upgr2wlk  26620  erclwwlkref  26977  erclwwlknref  27033  0spth  27104  0crct  27111  pjimai  29163  dfrp2  29660  eulerpartlemt0  30559  bnj1101  30981  bj-snglc  33082  icorempt2  33329  wl-cases2-dnf  33425  matunitlindf  33537  pm11.58  38907
  Copyright terms: Public domain W3C validator