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  1274  elrabf  2672  sbcco  2761  sbc5  2763  sbcan  2781  sbcor  2783  sbcal  2786  sbcex2  2788  eldif  2903  elun  3060  elin  3102  eluni  3556  eliun  3634  elopab  3968  opelopabsb  3970  opeliunxp  4320  opeliunxp2  4401  elxp4  4733  elxp5  4734  fsn2  5260  isocnv2  5375  elxp6  5716  elxp7  5717  brtpos2  5785  tpostpos  5798  ecdmn0m  6053  elinp  6313
  Copyright terms: Public domain W3C validator