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 550
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 548 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))
31, 2mpbi 221 1 (𝜑 ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  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 198  df-an 384
This theorem is referenced by:  pm4.24  554  anabs1  642  pm4.45  1009  2eu5  2709  rabeqc  3519  imadmrn  5627  dff1o2  6298  f12dfv  6691  isof1oidb  6736  isof1oopb  6737  xpsnen  8221  dom0  8265  dfac5lem2  9168  pwfseqlem4  9707  axgroth6  9873  eqreznegel  11999  xrnemnf  12173  xrnepnf  12174  elioopnf  12492  elioomnf  12493  elicopnf  12494  elxrge0  12507  isprm2  15623  efgrelexlemb  18390  opsrtoslem1  19719  tgphaus  22160  cfilucfil3  23356  ioombl1lem4  23569  vitalilem1  23616  ellogdm  24627  nb3grpr2  26529  upgr2wlk  26820  erclwwlkref  27191  erclwwlknref  27248  0spth  27327  0crct  27334  pjimai  29392  dfrp2  29889  eulerpartlemt0  30788  bnj1101  31210  bj-snglc  33305  icorempt2  33553  wl-cases2-dnf  33649  matunitlindf  33757  pm11.58  39130
  Copyright terms: Public domain W3C validator