MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.21nii Unicode version

Theorem pm5.21nii 353
Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.)
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.21nii.3 . 2
2 pm5.21ni.1 . . 3
3 pm5.21ni.2 . . 3
42, 3pm5.21ni 352 . 2
51, 4pm2.61i 164 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  elrabf  3255  sbcco  3350  sbc5  3352  sbcan  3370  sbcor  3372  sbcal  3379  sbcex2  3381  sbcel1v  3392  sbcreu  3414  eldif  3485  elun  3644  elin  3686  sbccsb2  3851  eluni  4252  eliun  4335  elopab  4760  opelopabsb  4762  opeliunxp2  5146  elpwun  6613  elxp5  6745  tpostpos  6994  ecdmn0  7373  brecop2  7424  elixpsn  7528  bren  7545  elharval  8010  sdom2en01  8703  isfin1-2  8786  wdomac  8926  elwina  9085  elina  9086  lterpq  9369  ltrnq  9378  elnp  9386  elnpi  9387  ltresr  9538  eluz2  11116  dfle2  11382  dflt2  11383  rexanuz2  13182  isstruct2  14641  xpsfrnel2  14962  ismre  14987  isacs  15048  brssc  15183  isfunc  15233  oduclatb  15774  isipodrs  15791  issubg  16201  isnsg  16230  oppgsubm  16397  oppgsubg  16398  isslw  16628  efgrelexlema  16767  dvdsr  17295  isunit  17306  isirred  17348  issubrg  17429  opprsubrg  17450  islss  17581  islbs4  18867  eltopspOLD  19419  istpsOLD  19421  istopon  19426  basdif0  19454  dis2ndc  19961  elmptrab  20328  isusp  20764  ismet2  20836  isphtpc  21494  elpi1  21545  iscmet  21723  bcthlem1  21763  isvc  25474  isnv  25505  hlimi  26105  h1de2ci  26474  elunop  26791  ispcmp  27860  elmpps  28933  eldm3  29191  opelco3  29208  elima4  29209  elno  29406  brsset  29539  brbigcup  29548  elfix2  29554  elsingles  29568  imageval  29580  funpartlem  29592  elaltxp  29625  ellines  29802  isfne4  30158  istotbnd  30265  isbnd  30276  isdrngo1  30359  isnacs  30636  sbccomieg  30726  inisegn0  30989  elmnc  31085  2reu4  32195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator