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

Theorem syl6ibr 221
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6ibr.1
syl6ibr.2
Assertion
Ref Expression
syl6ibr

Proof of Theorem syl6ibr
StepHypRef Expression
1 syl6ibr.1 . 2
2 syl6ibr.2 . . 3
32biimpri 200 . 2
41, 3syl6 32 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178
This theorem is referenced by:  3imtr4g  264  imp4a  576  3impexpbicom  1403  nic-ax  1474  nfimd  1840  mo2v  2250  euim  2310  mopick2  2333  2moswap  2341  2eu1  2347  necon3ad  2623  necon3d  2625  necon1d  2659  ralrimd  2783  spcimegf  3029  spcegf  3031  spcimedv  3034  spc2gv  3038  spc3gv  3040  rspcimedv  3053  eqsbc3r  3225  ra4  3259  tpid3g  3965  pwpw0  3996  sssn  4006  pwsnALT  4061  ssiun  4187  ssiun2  4188  reusv6OLD  4475  wefrc  4685  tron  4713  ordtri3or  4722  oneqmini  4741  dmcosseq  5072  relssres  5119  restidsing  5134  trin2  5193  ssrnres  5248  sossfld  5257  fnun  5487  f1oun  5630  brprcneu  5654  ssimaex  5726  chfnrn  5784  dffo4  5829  dffo5  5830  fvclss  5927  isomin  5996  isofrlem  5999  isoselem  6000  fnoprabg  6161  nnsuc  6463  f1oweALT  6530  bropopvvv  6622  frxp  6651  poxp  6653  fnse  6658  mpt2xopynvov0g  6693  issmo2  6769  smores  6772  smogt  6787  rdglim2  6847  tz7.48lem  6855  tz7.49  6859  swoer  7090  qsss  7122  domtriord  7416  pssnn  7490  ssfi  7492  findcard  7510  findcard2  7511  findcard3  7514  frfi  7516  dffi3  7628  supmo  7649  inf3lem4  7784  carddom2  8094  fidomtri2  8111  pm54.43  8117  infpwfien  8179  alephordi  8191  cardaleph  8206  carduniima  8213  cardinfima  8214  alephval3  8227  dfac5lem4  8243  dfac5  8245  dfac2  8247  kmlem2  8267  cflm  8366  cfslb2n  8384  cfsmolem  8386  isf32lem9  8477  axcc4  8555  domtriomlem  8558  zorn2lem4  8615  zorn2lem6  8617  fpwwe2lem11  8753  fpwwe2lem12  8754  inttsk  8887  inar1  8888  intgru  8927  ingru  8928  indpi  9022  nqpr  9129  ltaddpr  9149  ltexprlem1  9151  ltexprlem5  9155  reclem2pr  9163  reclem4pr  9165  zmulcl  10638  uzm1  10836  uzwo  10862  uzwoOLD  10863  negn0  10886  xmullem2  11173  icoshft  11351  difreicc  11361  fzouzsplit  11525  ssfzoulel  11562  seqf1olem1  11786  seqf1olem2  11787  hashtpg  12127  swrdnd  12267  swrdccatin2  12319  incexclem  13239  sqr2irr  13471  dvds2lem  13485  dvdslelem  13517  divalglem8  13544  euclemma  13734  iserodd  13842  ramcl  14030  mreiincl  14474  joinfval  15111  meetfval  15125  dirge  15347  sylow2alem1  16053  efgredlemb  16180  lbspss  16972  lspsneu  17013  lspsnat  17035  lspsncv0  17036  opsrtoslem2  17368  distop  18304  epttop  18317  isclo2  18396  restdis  18486  subbascn  18562  cnrest2  18594  cnpresti  18596  isnrm2  18666  cmpsublem  18706  cmpcld  18709  dfcon2  18727  t1conperf  18744  1stcrest  18761  lly1stc  18804  uptx  18902  txcn  18903  prdstopn  18905  txcon  18966  cmphaushmeo  19077  fbasrn  19161  csdfil  19171  trufil  19187  fclscf  19302  alexsubALTlem3  19325  alexsubALT  19327  haustsms2  19411  ovoliunlem1  20685  ovoliunnul  20690  volsup2  20785  coeaddlem  21457  plymul0or  21488  radcnv0  21622  wilthlem3  22149  chtub  22292  2sqlem10  22454  pntpbnd1  22576  mptelee  22820  axeuclidlem  22887  axcontlem4  22892  usgrarnedg  22982  usgraedg4  22984  isch3  24323  shmodsi  24471  orthin  24528  h1datomi  24663  stcltr2i  25358  atom1d  25436  sumdmdii  25498  cdj3lem1  25517  disjpreima  25608  suppss3  25707  kerf1hrm  26000  lmxrge0  26091  dmvlsiga  26281  sibfof  26429  erdszelem9  26790  cvmlift2lem1  26894  fundmpss  27279  tfisg  27367  wfisg  27372  frinsg  27408  poseq  27416  sltval2  27499  nodenselem7  27530  nofulllem5  27549  outsideofrflx  27860  mblfinlem3  28101  itg2addnclem3  28116  nn0prpwlem  28188  ivthALT  28201  fnessref  28236  neibastop2lem  28252  tailfb  28269  cover2  28278  fdc  28312  nninfnub  28318  equivtotbnd  28348  prdstotbnd  28364  cntotbnd  28366  ablo4pnp  28416  isdrngo3  28436  crngohomfo  28477  intidl  28500  or32dd  28568  prtlem90  28674  prtlem18  28694  prter2  28698  2reu1  29684  modfsummod  29919  lswn0  29932  frgrancvvdeqlemA  30304  frgrancvvdeqlemC  30306  alrim3con13v  30816  tratrb  30819  onfrALTlem3  30829  onfrALTlem2  30831  onfrALTlem1  30833  trsspwALT2  31131  trsspwALT3  31132  bnj600  31490  bnj1018  31533  bnj1173  31571  bnj1174  31572  bj-axtd  31666  bj-2upleq  31952  lsat0cv  32115  lfl1  32152  lkreqN  32252  atlrelat1  32403  pmaple  32842  pmapsub  32849  pclclN  32972  pclfinN  32981  osumcllem4N  33040  pexmidlem1N  33051  cdleme7ga  33329  lcfl7N  34583
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 179
  Copyright terms: Public domain W3C validator