MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.71d Structured version   Visualization version   GIF version

Theorem pm4.71d 669
Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by Mario Carneiro, 25-Dec-2016.)
Hypothesis
Ref Expression
pm4.71rd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
pm4.71d (𝜑 → (𝜓 ↔ (𝜓𝜒)))

Proof of Theorem pm4.71d
StepHypRef Expression
1 pm4.71rd.1 . 2 (𝜑 → (𝜓𝜒))
2 pm4.71 665 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜓𝜒)))
31, 2sylib 208 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:  difin2  4033  resopab2  5606  ordtri3  5920  fcnvres  6243  resoprab2  6923  psgnran  18155  efgcpbllemb  18388  cndis  21317  cnindis  21318  cnpdis  21319  blpnf  22423  dscopn  22599  itgcn  23828  limcnlp  23861  nb3gr2nb  26505  uspgr2wlkeq  26773  upgrspthswlk  26865  wspthsnwspthsnon  27055  wspthsnwspthsnonOLD  27057  wpthswwlks2on  27103  wpthswwlks2onOLD  27104  1stpreima  29814  fsumcvg4  30326  mbfmcnt  30660  topdifinffinlem  33524  phpreu  33724  ptrest  33739  rngosn3  34054  isidlc  34145  dih1  37095  lzunuz  37851  fsovrfovd  38823  uneqsn  38841
  Copyright terms: Public domain W3C validator