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 560
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 558 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))
31, 2mpbi 231 1 (𝜑 ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  pm4.71ri  561  pm4.24  564  anabs1  658  pm4.45im  823  pm4.45  991  eu6lem  2654  2eu5  2738  2eu5OLD  2739  rabeqc  3677  imadmrn  5933  dff1o2  6614  f12dfv  7021  isof1oidb  7066  isof1oopb  7067  xpsnen  8590  dom0  8634  dfac5lem2  9539  pwfseqlem4  10073  axgroth6  10239  eqreznegel  12323  xrnemnf  12502  xrnepnf  12503  elioopnf  12821  elioomnf  12822  elicopnf  12823  elxrge0  12835  isprm2  16016  efgrelexlemb  18807  opsrtoslem1  20194  tgphaus  22654  cfilucfil3  23852  ioombl1lem4  24091  vitalilem1  24138  ellogdm  25149  nb3grpr2  27093  upgr2wlk  27378  erclwwlkref  27726  erclwwlknref  27776  0spth  27833  0crct  27840  pjimai  29881  dfrp2  30418  eulerpartlemt0  31527  bnj1101  31956  satfvsuclem2  32505  bj-snglc  34179  bj-epelb  34256  bj-opelidb1  34338  icorempo  34515  wl-cases2-dnf  34635  matunitlindf  34772  pm11.58  40602
  Copyright terms: Public domain W3C validator