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 562
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 558 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜓𝜒)))
31, 2sylib 219 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.71rd  563  difin2  4192  resopab2  5792  ordtri3  6109  resoprab2  7134  psgnran  18378  efgcpbllemb  18612  cndis  21587  cnindis  21588  cnpdis  21589  blpnf  22694  dscopn  22870  itgcn  24130  limcnlp  24163  2sqreultlem  25709  2sqreunnltlem  25712  dfcgrg2  26336  nb3gr2nb  26853  uspgr2wlkeq  27114  upgrspthswlk  27205  wspthsnwspthsnon  27381  wpthswwlks2on  27426  1stpreima  30126  cntzsnid  30503  fsumcvg4  30806  mbfmcnt  31139  satfv0  32215  topdifinffinlem  34180  phpreu  34428  ptrest  34443  rngosn3  34755  isidlc  34846  dih1  37974  rabeqcda  38657  prjsperref  38774  lzunuz  38871  fsovrfovd  39861  uneqsn  39879  itsclquadeu  44267
  Copyright terms: Public domain W3C validator