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 563
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 559 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜓𝜒)))
31, 2sylib 217 1 (𝜑 → (𝜓 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  pm4.71rd  564  rabeqcda  3417  difin2  4255  resopab2  5994  ordtri3  6357  onunel  6426  resoprab2  7479  psgnran  19305  efgcpbllemb  19545  cndis  22665  cnindis  22666  cnpdis  22667  blpnf  23773  dscopn  23952  itgcn  25232  limcnlp  25265  2sqreultlem  26818  2sqreunnltlem  26821  dfcgrg2  27854  nb3gr2nb  28381  uspgr2wlkeq  28643  upgrspthswlk  28735  wspthsnwspthsnon  28910  wpthswwlks2on  28955  1stpreima  31674  cntzsnid  31959  qusxpid  32205  ressply1mon1p  32334  fsumcvg4  32595  mbfmcnt  32932  satfv0  34016  topdifinffinlem  35868  phpreu  36112  ptrest  36127  rngosn3  36433  isidlc  36524  dih1  39799  prjsperref  40991  lzunuz  41138  nadd1suc  41755  naddsuc2  41756  fsovrfovd  42373  uneqsn  42389  itsclquadeu  46953  pm4.71da  46965  i0oii  47042  io1ii  47043
  Copyright terms: Public domain W3C validator