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

Theorem pm5.21nii 658
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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  anxordi  1343  elrabf  2783  sbcco  2875  sbc5  2877  sbcan  2895  sbcor  2897  sbcal  2904  sbcex2  2906  sbcel1v  2915  eldif  3022  elun  3156  elin  3198  eluni  3678  eliun  3756  elopab  4109  opelopabsb  4111  opeliunxp  4522  opeliunxp2  4607  elxp4  4952  elxp5  4953  fsn2  5510  isocnv2  5629  elxp6  5978  elxp7  5979  opeliunxp2f  6041  brtpos2  6054  tpostpos  6067  ecdmn0m  6374  elixpsn  6532  bren  6544  elinp  7130  recexprlemell  7278  recexprlemelu  7279  gt0srpr  7391  ltresr  7473  eluz2  9124  elfz2  9580  rexanuz2  10539  even2n  11301  infssuzex  11372  istopon  11864  ismet2  12140
  Copyright terms: Public domain W3C validator