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

Theorem pm5.21ndd 705
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 178 . 2 (𝜑 → (𝜒𝜃))
5 pm5.21ndd.2 . . . . 5 (𝜑 → (𝜃𝜓))
65, 2syld 45 . . . 4 (𝜑 → (𝜃 → (𝜒𝜃)))
7 bicom1 131 . . . 4 ((𝜒𝜃) → (𝜃𝜒))
86, 7syl6 33 . . 3 (𝜑 → (𝜃 → (𝜃𝜒)))
98ibd 178 . 2 (𝜑 → (𝜃𝜒))
104, 9impbid 129 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  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:  pm5.21nd  916  sbcrext  3042  rmob  3057  epelg  4292  eqbrrdva  4799  elrelimasn  4996  relbrcnvg  5009  fmptco  5684  ovelrn  6025  brtpos2  6254  elpmg  6666  brdomg  6750  elfi2  6973  genpelvl  7513  genpelvu  7514  fzoval  10150  clim  11291  dvdsaddre2b  11850  pceu  12297  mndpropd  12846  issubg3  13057  dvdsrd  13268  subrgpropd  13374  lmodprop2d  13443  cnrest2  13821  cnptoprest2  13825  lmss  13831  reopnap  14123  limcdifap  14216
  Copyright terms: Public domain W3C validator