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

Theorem pm5.21nii 383
 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 382 . 2 𝜓 → (𝜑𝜒))
51, 4pm2.61i 185 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  elrabf  3624  elrab  3628  sbccow  3743  sbcco  3746  sbc5  3748  sbcan  3768  sbcor  3769  sbcal  3780  sbcex2  3781  sbcel1v  3786  sbcreu  3805  eldif  3891  elin  3897  elun  4076  sbccsb2  4342  2reu4  4424  elpr2OLD  4551  eluni  4804  eliun  4886  sbcbr123  5085  elopab  5380  opelopabsb  5383  opeliunxp2  5674  inisegn0  5929  brfvopabrbr  6743  elpwun  7474  elxp5  7613  opeliunxp2f  7862  tpostpos  7898  ecdmn0  8322  brecop2  8377  elixpsn  8487  bren  8504  elharval  9012  sdom2en01  9716  isfin1-2  9799  wdomac  9941  elwina  10100  elina  10101  lterpq  10384  ltrnq  10393  elnp  10401  elnpi  10402  ltresr  10554  eluz2  12240  dfle2  12531  dflt2  12532  rexanuz2  14704  even2n  15686  isstruct2  16488  xpsfrnel2  16832  ismre  16856  isacs  16917  brssc  17079  isfunc  17129  oduclatb  17749  isipodrs  17766  issubg  18275  isnsg  18303  oppgsubm  18486  oppgsubg  18487  isslw  18729  efgrelexlema  18871  dvdsr  19396  isunit  19407  isirred  19449  issubrg  19532  opprsubrg  19553  islss  19703  islbs4  20526  istopon  21527  basdif0  21568  dis2ndc  22075  elmptrab  22442  isusp  22877  ismet2  22950  isphtpc  23609  elpi1  23660  iscmet  23898  bcthlem1  23938  wlkcpr  27428  isvcOLD  28372  isnv  28405  hlimi  28981  h1de2ci  29349  elunop  29665  ispcmp  31225  elmpps  32948  eldm3  33125  opelco3  33146  elima4  33147  elno  33281  brsset  33478  brbigcup  33487  elfix2  33493  elsingles  33507  imageval  33519  funpartlem  33531  elaltxp  33564  ellines  33741  isfne4  33816  bj-ismoore  34539  bj-idreseqb  34597  istotbnd  35226  isbnd  35237  isdrngo1  35413  isnacs  39688  sbccomieg  39777  elmnc  40123  ismea  43133
 Copyright terms: Public domain W3C validator