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

Theorem pm5.21nii 653
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 174 . 2 (𝜑𝜒)
5 pm5.21ni.2 . . . 4 (𝜒𝜓)
65, 2syl 14 . . 3 (𝜒 → (𝜑𝜒))
76ibir 175 . 2 (𝜒𝜑)
84, 7impbii 124 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  anxordi  1334  elrabf  2759  sbcco  2849  sbc5  2851  sbcan  2869  sbcor  2871  sbcal  2878  sbcex2  2880  sbcel1v  2889  eldif  2995  elun  3127  elin  3169  eluni  3633  eliun  3711  elopab  4052  opelopabsb  4054  opeliunxp  4454  opeliunxp2  4537  elxp4  4875  elxp5  4876  fsn2  5416  isocnv2  5534  elxp6  5878  elxp7  5879  brtpos2  5951  tpostpos  5964  ecdmn0m  6267  bren  6397  elinp  6954  recexprlemell  7102  recexprlemelu  7103  gt0srpr  7215  ltresr  7297  eluz2  8934  elfz2  9340  rexanuz2  10265  even2n  10668  infssuzex  10739
  Copyright terms: Public domain W3C validator