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 551
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 547 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜓𝜒)))
31, 2sylib 208 1 (𝜑 → (𝜓 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 383
This theorem is referenced by:  difin2  4038  resopab2  5587  ordtri3  5900  fcnvres  6220  resoprab2  6904  psgnran  18138  efgcpbllemb  18371  cndis  21312  cnindis  21313  cnpdis  21314  blpnf  22418  dscopn  22594  itgcn  23825  limcnlp  23858  nb3gr2nb  26505  uspgr2wlkeq  26773  upgrspthswlk  26865  wspthsnwspthsnon  27057  wspthsnwspthsnonOLD  27059  wpthswwlks2on  27105  wpthswwlks2onOLD  27106  1stpreima  29820  fsumcvg4  30332  mbfmcnt  30666  topdifinffinlem  33528  phpreu  33722  ptrest  33737  rngosn3  34051  isidlc  34142  dih1  37093  lzunuz  37854  fsovrfovd  38826  uneqsn  38844
  Copyright terms: Public domain W3C validator