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

Theorem pm5.21nii 620
 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  1291  elrabf  2696  sbcco  2785  sbc5  2787  sbcan  2805  sbcor  2807  sbcal  2810  sbcex2  2812  eldif  2927  elun  3084  elin  3126  eluni  3583  eliun  3661  elopab  3995  opelopabsb  3997  opeliunxp  4395  opeliunxp2  4476  elxp4  4808  elxp5  4809  fsn2  5337  isocnv2  5452  elxp6  5796  elxp7  5797  brtpos2  5866  tpostpos  5879  ecdmn0m  6148  bren  6228  elinp  6572  recexprlemell  6720  recexprlemelu  6721  gt0srpr  6833  ltresr  6915  eluz2  8479  elfz2  8881  rexanuz2  9589
 Copyright terms: Public domain W3C validator