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  3444  difin2  4289  resopab2  6033  ordtri3  6396  onunel  6465  resoprab2  7521  psgnran  19375  efgcpbllemb  19615  cndis  22776  cnindis  22777  cnpdis  22778  blpnf  23884  dscopn  24063  itgcn  25343  limcnlp  25376  2sqreultlem  26929  2sqreunnltlem  26932  dfcgrg2  28093  nb3gr2nb  28620  uspgr2wlkeq  28882  upgrspthswlk  28974  wspthsnwspthsnon  29149  wpthswwlks2on  29194  1stpreima  31905  cntzsnid  32190  qusxpid  32443  qsfld  32564  ressply1mon1p  32603  fsumcvg4  32867  mbfmcnt  33204  satfv0  34286  topdifinffinlem  36165  phpreu  36409  ptrest  36424  rngosn3  36729  isidlc  36820  dih1  40094  prjsperref  41291  lzunuz  41438  nadd1suc  42074  naddsuc2  42075  fsovrfovd  42692  uneqsn  42708  itsclquadeu  47364  pm4.71da  47376  i0oii  47453  io1ii  47454
  Copyright terms: Public domain W3C validator