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 563
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 561 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))
31, 2mpbi 233 1 (𝜑 ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  pm4.71ri  564  pm4.24  567  anabs1  662  pm4.45im  827  pm4.45  997  eu6lem  2575  2eu5  2659  rabeqc  3591  imadmrn  5923  dff1o2  6635  f12dfv  7053  isof1oidb  7102  isof1oopb  7103  xpsnen  8662  dom0  8707  dfac5lem2  9636  pwfseqlem4  10174  axgroth6  10340  eqreznegel  12428  xrnemnf  12607  xrnepnf  12608  dfrp2  12882  elioopnf  12929  elioomnf  12930  elicopnf  12931  elxrge0  12943  isprm2  16135  efgrelexlemb  19006  opsrtoslem1  20878  tgphaus  22880  cfilucfil3  24084  ioombl1lem4  24325  vitalilem1  24372  ellogdm  25394  nb3grpr2  27337  upgr2wlk  27622  erclwwlkref  27969  erclwwlknref  28018  0spth  28075  0crct  28082  pjimai  30123  eulerpartlemt0  31918  bnj1101  32347  satfvsuclem2  32905  bj-snglc  34814  bj-epelb  34894  bj-opelidb1  34977  icorempo  35177  wl-cases2-dnf  35326  matunitlindf  35430  pm11.58  41586
  Copyright terms: Public domain W3C validator