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

Theorem pm5.21nii 705
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 176 . 2 (𝜑𝜒)
5 pm5.21ni.2 . . . 4 (𝜒𝜓)
65, 2syl 14 . . 3 (𝜒 → (𝜑𝜒))
76ibir 177 . 2 (𝜒𝜑)
84, 7impbii 126 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  anxordi  1410  elrabf  2903  sbcco  2996  sbc5  2998  sbcan  3017  sbcor  3019  sbcal  3026  sbcex2  3028  sbcel1v  3037  eldif  3150  elun  3288  elin  3330  eluni  3824  eliun  3902  elopab  4270  opelopabsb  4272  opeliunxp  4693  opeliunxp2  4779  elxp4  5128  elxp5  5129  fsn2  5703  isocnv2  5826  elxp6  6183  elxp7  6184  opeliunxp2f  6252  brtpos2  6265  tpostpos  6278  ecdmn0m  6590  elixpsn  6748  bren  6760  omniwomnimkv  7178  elinp  7486  recexprlemell  7634  recexprlemelu  7635  gt0srpr  7760  ltresr  7851  eluz2  9547  elfz2  10028  rexanuz2  11013  even2n  11892  infssuzex  11963  infpn2  12470  xpsfrnel2  12783  issubg  13064  isnsg  13093  issrg  13212  iscrng2  13262  issubrng  13414  issubrg  13436  islssm  13541  islidlm  13663  2idlelb  13684  istopon  13784  ishmeo  14075  ismet2  14125
  Copyright terms: Public domain W3C validator