ILE Home 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  2693  sbcco  2782  sbc5  2784  sbcan  2802  sbcor  2804  sbcal  2807  sbcex2  2809  eldif  2924  elun  3081  elin  3123  eluni  3580  eliun  3658  elopab  3992  opelopabsb  3994  opeliunxp  4382  opeliunxp2  4463  elxp4  4795  elxp5  4796  fsn2  5324  isocnv2  5439  elxp6  5783  elxp7  5784  brtpos2  5853  tpostpos  5866  ecdmn0m  6135  bren  6215  elinp  6553  recexprlemell  6701  recexprlemelu  6702  gt0srpr  6814  ltresr  6896  eluz2  8451  elfz2  8848  rexanuz2  9467
  Copyright terms: Public domain W3C validator