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

Theorem syl6ibr 227
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 10-Jan-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 206 . 2
41, 3syl6 33 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3imtr4g  270  imp4a  589  nic-ax  1481  nfimd  1855  mo2v  2269  mo2vOLD  2270  mo2vOLDOLD  2271  euim  2333  mopick2  2357  2moswap  2365  2eu1OLD  2374  2eu6  2380  necon3adOLD  2664  necon3d  2677  necon1d  2678  ralrimd  2912  spcimegf  3160  spcegf  3162  spcimedv  3165  spc2gv  3169  spc3gv  3171  rspcimedv  3184  eqsbc3r  3359  ra4  3393  tpid3g  4107  pwpw0  4138  sssn  4148  pwsnALT  4203  ssiun  4329  ssiun2  4330  reusv6OLD  4620  wefrc  4831  tron  4859  ordtri3or  4868  oneqmini  4887  dmcosseq  5218  relssres  5265  restidsing  5281  trin2  5340  ssrnres  5395  sossfld  5404  fnun  5636  f1oun  5782  brprcneu  5806  ssimaex  5879  chfnrn  5937  dffo4  5982  dffo5  5983  fvclss  6084  isomin  6159  isofrlem  6162  isoselem  6163  fnoprabg  6324  nnsuc  6626  f1oweALT  6694  bropopvvv  6786  frxp  6816  poxp  6818  fnse  6823  mpt2xopynvov0g  6865  issmo2  6944  smores  6947  smogt  6962  rdglim2  7022  tz7.48lem  7030  tz7.49  7034  swoer  7263  qsss  7295  domtriord  7591  pssnn  7666  ssfi  7668  findcard  7686  findcard2  7687  findcard3  7690  frfi  7692  dffi3  7817  supmo  7838  inf3lem4  7974  carddom2  8284  fidomtri2  8301  pm54.43  8307  infpwfien  8369  alephordi  8381  cardaleph  8396  carduniima  8403  cardinfima  8404  alephval3  8417  dfac5lem4  8433  dfac5  8435  dfac2  8437  kmlem2  8457  cflm  8556  cfslb2n  8574  cfsmolem  8576  isf32lem9  8667  axcc4  8745  domtriomlem  8748  zorn2lem4  8805  zorn2lem6  8807  fpwwe2lem11  8944  fpwwe2lem12  8945  inttsk  9078  inar1  9079  intgru  9118  ingru  9119  indpi  9213  nqpr  9320  ltaddpr  9340  ltexprlem1  9342  ltexprlem5  9346  reclem2pr  9354  reclem4pr  9356  zmulcl  10831  uzm1  11030  uzwo  11056  uzwoOLD  11057  negn0  11080  xmullem2  11367  icoshft  11552  difreicc  11562  fzouzsplit  11729  ssfzoulel  11766  seqf1olem1  12002  seqf1olem2  12003  hashtpg  12344  swrdnd  12484  swrdccatin2  12536  incexclem  13457  sqr2irr  13689  dvds2lem  13703  dvdslelem  13735  divalglem8  13762  euclemma  13952  iserodd  14060  ramcl  14248  mreiincl  14693  joinfval  15330  meetfval  15344  dirge  15566  sylow2alem1  16277  efgredlemb  16404  kerf1hrm  17007  lbspss  17339  lspsneu  17380  lspsnat  17402  lspsncv0  17403  opsrtoslem2  17743  distop  18999  epttop  19012  isclo2  19091  restdis  19181  subbascn  19257  cnrest2  19289  cnpresti  19291  isnrm2  19361  cmpsublem  19401  cmpcld  19404  dfcon2  19422  t1conperf  19439  1stcrest  19456  lly1stc  19499  uptx  19597  txcn  19598  prdstopn  19600  txcon  19661  cmphaushmeo  19772  fbasrn  19856  csdfil  19866  trufil  19882  fclscf  19997  alexsubALTlem3  20020  alexsubALT  20022  haustsms2  20106  ovoliunlem1  21384  ovoliunnul  21389  volsup2  21485  coeaddlem  22116  plymul0or  22147  radcnv0  22281  wilthlem3  22808  chtub  22951  2sqlem10  23113  pntpbnd1  23235  mptelee  23610  axeuclidlem  23677  axcontlem4  23682  usgrarnedg  23772  usgraedg4  23774  isch3  25113  shmodsi  25261  orthin  25318  h1datomi  25453  stcltr2i  26148  atom1d  26226  sumdmdii  26288  cdj3lem1  26307  disjpreima  26396  suppss3  26494  lmxrge0  26839  dmvlsiga  27029  sibfof  27182  erdszelem9  27543  cvmlift2lem1  27647  fundmpss  28033  tfisg  28121  wfisg  28126  frinsg  28162  poseq  28170  sltval2  28253  nodenselem7  28284  nofulllem5  28303  outsideofrflx  28614  mblfinlem3  28890  itg2addnclem3  28905  nn0prpwlem  28977  ivthALT  28990  fnessref  29025  neibastop2lem  29041  tailfb  29058  cover2  29067  fdc  29101  nninfnub  29107  equivtotbnd  29137  prdstotbnd  29153  cntotbnd  29155  ablo4pnp  29205  isdrngo3  29225  crngohomfo  29266  intidl  29289  or32dd  29357  prtlem90  29462  prtlem18  29482  prter2  29486  2reu1  30887  modfsummod  31122  lswn0  31135  frgrancvvdeqlemA  31507  frgrancvvdeqlemC  31509  3impexpbicom  31999  alrim3con13v  32082  tratrb  32085  onfrALTlem3  32095  onfrALTlem2  32097  onfrALTlem1  32099  trsspwALT2  32396  trsspwALT3  32397  bnj600  32755  bnj1018  32798  bnj1173  32836  bnj1174  32837  bj-axtd  32963  bj-nfdt0  33029  bj-2upleq  33350  lsat0cv  33529  lfl1  33566  lkreqN  33666  atlrelat1  33817  pmaple  34256  pmapsub  34263  pclclN  34386  pclfinN  34395  osumcllem4N  34454  pexmidlem1N  34465  cdleme7ga  34743  lcfl7N  35997
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