ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm4.71rd GIF version

Theorem pm4.71rd 394
Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.)
Hypothesis
Ref Expression
pm4.71rd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
pm4.71rd (𝜑 → (𝜓 ↔ (𝜒𝜓)))

Proof of Theorem pm4.71rd
StepHypRef Expression
1 pm4.71rd.1 . 2 (𝜑 → (𝜓𝜒))
2 pm4.71r 390 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜒𝜓)))
31, 2sylib 122 1 (𝜑 → (𝜓 ↔ (𝜒𝜓)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ralss  3221  rexss  3222  reuhypd  4468  elxp4  5112  elxp5  5113  dfco2a  5125  feu  5394  funbrfv2b  5556  dffn5im  5557  eqfnfv2  5610  dff4im  5658  fmptco  5678  dff13  5763  f1od2  6230  mpoxopovel  6236  brtposg  6249  dftpos3  6257  erinxp  6603  qliftfun  6611  genpdflem  7494  ltexprlemm  7587  prime  9338  oddnn02np1  11865  oddge22np1  11866  evennn02n  11867  evennn2n  11868  ismgmid  12685  bastop2  13248  restopn2  13347  restdis  13348  tx1cn  13433  tx2cn  13434  imasnopn  13463  xmeter  13600
  Copyright terms: Public domain W3C validator