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

Theorem pm4.71d 664
 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 660 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜓𝜒)))
31, 2sylib 207 1 (𝜑 → (𝜓 ↔ (𝜓𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ 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 196  df-an 385 This theorem is referenced by:  difin2  3849  resopab2  5368  ordtri3  5676  fcnvres  5995  resoprab2  6655  psgnran  17758  efgcpbllemb  17991  cndis  20905  cnindis  20906  cnpdis  20907  blpnf  22012  dscopn  22188  itgcn  23415  limcnlp  23448  nb3gra2nb  25984  usg2wlkeq  26236  clwwlkn2  26303  1stpreima  28867  fsumcvg4  29324  mbfmcnt  29657  topdifinffinlem  32371  phpreu  32563  ptrest  32578  rngosn3  32893  isidlc  32984  dih1  35593  lzunuz  36349  fsovrfovd  37323  uneqsn  37341  nb3gr2nb  40612  uspgr2wlkeq  40854  upgrspths1wlk  40944  wspthsnwspthsnon  41122  wpthswwlks2on  41164
 Copyright terms: Public domain W3C validator