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 553
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 549 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜓𝜒)))
31, 2sylib 209 1 (𝜑 → (𝜓 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  difin2  4091  resopab2  5653  ordtri3  5972  fcnvres  6293  resoprab2  6983  psgnran  18132  efgcpbllemb  18365  cndis  21306  cnindis  21307  cnpdis  21308  blpnf  22412  dscopn  22588  itgcn  23822  limcnlp  23855  nb3gr2nb  26501  uspgr2wlkeq  26769  upgrspthswlk  26861  wspthsnwspthsnon  27053  wspthsnwspthsnonOLD  27055  wpthswwlks2on  27101  wpthswwlks2onOLD  27102  1stpreima  29810  fsumcvg4  30320  mbfmcnt  30654  topdifinffinlem  33509  phpreu  33704  ptrest  33719  rngosn3  34032  isidlc  34123  dih1  37064  lzunuz  37830  fsovrfovd  38800  uneqsn  38818
  Copyright terms: Public domain W3C validator