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 551
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 549 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))
31, 2mpbi 221 1 (𝜑 ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384
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 385
This theorem is referenced by:  pm4.24  555  anabs1  644  pm4.45  1011  2eu5  2721  rabeqc  3557  imadmrn  5686  dff1o2  6358  f12dfv  6753  isof1oidb  6798  isof1oopb  6799  xpsnen  8283  dom0  8327  dfac5lem2  9230  pwfseqlem4  9769  axgroth6  9935  eqreznegel  11993  xrnemnf  12167  xrnepnf  12168  elioopnf  12486  elioomnf  12487  elicopnf  12488  elxrge0  12501  isprm2  15613  efgrelexlemb  18364  opsrtoslem1  19692  tgphaus  22133  cfilucfil3  23329  ioombl1lem4  23542  vitalilem1  23589  ellogdm  24599  nb3grpr2  26501  upgr2wlk  26792  erclwwlkref  27163  erclwwlknref  27220  0spth  27299  0crct  27306  pjimai  29363  dfrp2  29859  eulerpartlemt0  30756  bnj1101  31178  bj-snglc  33267  icorempt2  33515  wl-cases2-dnf  33611  matunitlindf  33720  pm11.58  39090
  Copyright terms: Public domain W3C validator