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 663
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 659 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜓𝜒)))
31, 2sylib 206 1 (𝜑 → (𝜓 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  difin2  3848  resopab2  5355  ordtri3  5662  fcnvres  5980  resoprab2  6633  psgnran  17704  efgcpbllemb  17937  cndis  20847  cnindis  20848  cnpdis  20849  blpnf  21953  dscopn  22129  itgcn  23332  limcnlp  23365  nb3gra2nb  25750  usg2wlkeq  26002  clwwlkn2  26069  1stpreima  28673  fsumcvg4  29130  mbfmcnt  29463  topdifinffinlem  32167  phpreu  32359  ptrest  32374  rngosn3  32689  isidlc  32780  dih1  35389  lzunuz  36145  fsovrfovd  37119  uneqsn  37137  nb3gr2nb  40607  uspgr2wlkeq  40849  upgrspths1wlk  40939  wspthsnwspthsnon  41117  wpthswwlks2on  41159
  Copyright terms: Public domain W3C validator