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

Theorem pm4.71d 565
 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 561 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜓𝜒)))
31, 2sylib 221 1 (𝜑 → (𝜓 ↔ (𝜓𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  pm4.71rd  566  difin2  4219  resopab2  5875  ordtri3  6199  resoprab2  7254  psgnran  18639  efgcpbllemb  18877  cndis  21900  cnindis  21901  cnpdis  21902  blpnf  23008  dscopn  23184  itgcn  24452  limcnlp  24485  2sqreultlem  26035  2sqreunnltlem  26038  dfcgrg2  26661  nb3gr2nb  27178  uspgr2wlkeq  27439  upgrspthswlk  27531  wspthsnwspthsnon  27706  wpthswwlks2on  27751  1stpreima  30470  cntzsnid  30750  qusxpid  30983  fsumcvg4  31307  mbfmcnt  31640  satfv0  32719  topdifinffinlem  34765  phpreu  35040  ptrest  35055  rngosn3  35361  isidlc  35452  dih1  38581  rabeqcda  39395  prjsperref  39597  lzunuz  39706  fsovrfovd  40707  uneqsn  40723  itsclquadeu  45188
 Copyright terms: Public domain W3C validator