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

Theorem pm5.21nii 693
 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  1378  elrabf  2833  sbcco  2925  sbc5  2927  sbcan  2946  sbcor  2948  sbcal  2955  sbcex2  2957  sbcel1v  2966  eldif  3075  elun  3212  elin  3254  eluni  3734  eliun  3812  elopab  4175  opelopabsb  4177  opeliunxp  4589  opeliunxp2  4674  elxp4  5021  elxp5  5022  fsn2  5587  isocnv2  5706  elxp6  6060  elxp7  6061  opeliunxp2f  6128  brtpos2  6141  tpostpos  6154  ecdmn0m  6464  elixpsn  6622  bren  6634  elinp  7275  recexprlemell  7423  recexprlemelu  7424  gt0srpr  7549  ltresr  7640  eluz2  9325  elfz2  9790  rexanuz2  10756  even2n  11560  infssuzex  11631  istopon  12169  ishmeo  12462  ismet2  12512
 Copyright terms: Public domain W3C validator