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

Theorem pm5.21nii 607
Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypotheses
Ref Expression
pm5.21ni.1 (φψ)
pm5.21ni.2 (χψ)
pm5.21nii.3 (ψ → (φχ))
Assertion
Ref Expression
pm5.21nii (φχ)

Proof of Theorem pm5.21nii
StepHypRef Expression
1 pm5.21ni.1 . . . 4 (φψ)
2 pm5.21nii.3 . . . 4 (ψ → (φχ))
31, 2syl 14 . . 3 (φ → (φχ))
43ibi 165 . 2 (φχ)
5 pm5.21ni.2 . . . 4 (χψ)
65, 2syl 14 . . 3 (χ → (φχ))
76ibir 166 . 2 (χφ)
84, 7impbii 117 1 (φχ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  anxordi  1271  elrabf  2671  sbcco  2760  sbc5  2762  sbcan  2780  sbcor  2782  sbcal  2785  sbcex2  2787  eldif  2905  elun  3062  elin  3104  eluni  3535  eliun  3613  elopab  3947  opelopabsb  3950  opeliunxp  4288  opeliunxp2  4369  elxp4  4702  elxp5  4703  fsn2  5229  isocnv2  5344  elxp6  5685  elxp7  5686  brtpos2  5754  tpostpos  5767
  Copyright terms: Public domain W3C validator