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

Theorem pm5.21nii 619
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  1288  elrabf  2690  sbcco  2779  sbc5  2781  sbcan  2799  sbcor  2801  sbcal  2804  sbcex2  2806  eldif  2921  elun  3078  elin  3120  eluni  3574  eliun  3652  elopab  3986  opelopabsb  3988  opeliunxp  4338  opeliunxp2  4419  elxp4  4751  elxp5  4752  fsn2  5280  isocnv2  5395  elxp6  5738  elxp7  5739  brtpos2  5807  tpostpos  5820  ecdmn0m  6084  bren  6164  elinp  6456  recexprlemell  6593  recexprlemelu  6594  gt0srpr  6656  ltresr  6716  eluz2  8235  elfz2  8631
  Copyright terms: Public domain W3C validator