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

Theorem pm5.21nii 678
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 175 . 2 (𝜑𝜒)
5 pm5.21ni.2 . . . 4 (𝜒𝜓)
65, 2syl 14 . . 3 (𝜒 → (𝜑𝜒))
76ibir 176 . 2 (𝜒𝜑)
84, 7impbii 125 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  anxordi  1363  elrabf  2811  sbcco  2903  sbc5  2905  sbcan  2923  sbcor  2925  sbcal  2932  sbcex2  2934  sbcel1v  2943  eldif  3050  elun  3187  elin  3229  eluni  3709  eliun  3787  elopab  4150  opelopabsb  4152  opeliunxp  4564  opeliunxp2  4649  elxp4  4996  elxp5  4997  fsn2  5562  isocnv2  5681  elxp6  6035  elxp7  6036  opeliunxp2f  6103  brtpos2  6116  tpostpos  6129  ecdmn0m  6439  elixpsn  6597  bren  6609  elinp  7250  recexprlemell  7398  recexprlemelu  7399  gt0srpr  7524  ltresr  7615  eluz2  9300  elfz2  9765  rexanuz2  10731  even2n  11498  infssuzex  11569  istopon  12107  ishmeo  12400  ismet2  12450
  Copyright terms: Public domain W3C validator