ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm5.21ndd GIF version

Theorem pm5.21ndd 677
Description: Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypotheses
Ref Expression
pm5.21ndd.1 (𝜑 → (𝜒𝜓))
pm5.21ndd.2 (𝜑 → (𝜃𝜓))
pm5.21ndd.3 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
pm5.21ndd (𝜑 → (𝜒𝜃))

Proof of Theorem pm5.21ndd
StepHypRef Expression
1 pm5.21ndd.1 . . . 4 (𝜑 → (𝜒𝜓))
2 pm5.21ndd.3 . . . 4 (𝜑 → (𝜓 → (𝜒𝜃)))
31, 2syld 45 . . 3 (𝜑 → (𝜒 → (𝜒𝜃)))
43ibd 177 . 2 (𝜑 → (𝜒𝜃))
5 pm5.21ndd.2 . . . . 5 (𝜑 → (𝜃𝜓))
65, 2syld 45 . . . 4 (𝜑 → (𝜃 → (𝜒𝜃)))
7 bicom1 130 . . . 4 ((𝜒𝜃) → (𝜃𝜒))
86, 7syl6 33 . . 3 (𝜑 → (𝜃 → (𝜃𝜒)))
98ibd 177 . 2 (𝜑 → (𝜃𝜒))
104, 9impbid 128 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.21nd  884  sbcrext  2956  rmob  2971  epelg  4180  eqbrrdva  4677  relbrcnvg  4886  fmptco  5552  ovelrn  5885  brtpos2  6114  elpmg  6524  brdomg  6608  elfi2  6826  genpelvl  7284  genpelvu  7285  fzoval  9876  clim  11001  cnrest2  12311  cnptoprest2  12315  lmss  12321  reopnap  12613  limcdifap  12706
  Copyright terms: Public domain W3C validator