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

Theorem pm5.21ndd 656
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 44 . . 3 (𝜑 → (𝜒 → (𝜒𝜃)))
43ibd 176 . 2 (𝜑 → (𝜒𝜃))
5 pm5.21ndd.2 . . . . 5 (𝜑 → (𝜃𝜓))
65, 2syld 44 . . . 4 (𝜑 → (𝜃 → (𝜒𝜃)))
7 bicom1 129 . . . 4 ((𝜒𝜃) → (𝜃𝜒))
86, 7syl6 33 . . 3 (𝜑 → (𝜃 → (𝜃𝜒)))
98ibd 176 . 2 (𝜑 → (𝜃𝜒))
104, 9impbid 127 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.21nd  863  sbcrext  2914  rmob  2929  epelg  4108  eqbrrdva  4594  relbrcnvg  4798  fmptco  5448  ovelrn  5775  brtpos2  5998  elpmg  6401  brdomg  6445  genpelvl  7050  genpelvu  7051  fzoval  9524  clim  10633
  Copyright terms: Public domain W3C validator