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

Theorem pm5.21nii 604
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  1272  elrabf  2667  sbcco  2756  sbc5  2758  sbcan  2776  sbcor  2778  sbcal  2781  sbcex2  2783  eldif  2898  elun  3055  elin  3097  eluni  3549  eliun  3627  elopab  3961  opelopabsb  3963  opeliunxp  4313  opeliunxp2  4394  elxp4  4726  elxp5  4727  fsn2  5253  isocnv2  5368  elxp6  5710  elxp7  5711  brtpos2  5779  tpostpos  5792  ecdmn0m  6050  elinp  6317  recexprlemell  6446  recexprlemelu  6447  gt0srpr  6489  ltresr  6548  eluz2  8047
  Copyright terms: Public domain W3C validator