MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6ibr Structured version   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, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6ibr.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl6ibr.2  |-  ( th  <->  ch )
Assertion
Ref Expression
syl6ibr  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syl6ibr
StepHypRef Expression
1 syl6ibr.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl6ibr.2 . . 3  |-  ( th  <->  ch )
32biimpri 206 . 2  |-  ( ch 
->  th )
41, 3syl6 33 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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
This theorem is referenced by:  3imtr4g  270  imp4a  586  3impexpbicom  1416  nic-ax  1485  nfimd  1854  mo2v  2264  mo2vOLD  2265  euim  2327  mopick2  2351  2moswap  2359  2eu1  2365  necon3ad  2642  necon3d  2644  necon1d  2678  ralrimd  2802  spcimegf  3048  spcegf  3050  spcimedv  3053  spc2gv  3057  spc3gv  3059  rspcimedv  3072  eqsbc3r  3245  ra4  3279  tpid3g  3987  pwpw0  4018  sssn  4028  pwsnALT  4083  ssiun  4209  ssiun2  4210  reusv6OLD  4500  wefrc  4710  tron  4738  ordtri3or  4747  oneqmini  4766  dmcosseq  5097  relssres  5144  restidsing  5159  trin2  5218  ssrnres  5273  sossfld  5282  fnun  5514  f1oun  5657  brprcneu  5681  ssimaex  5753  chfnrn  5811  dffo4  5856  dffo5  5857  fvclss  5956  isomin  6025  isofrlem  6028  isoselem  6029  fnoprabg  6190  nnsuc  6492  f1oweALT  6560  bropopvvv  6652  frxp  6681  poxp  6683  fnse  6688  mpt2xopynvov0g  6730  issmo2  6806  smores  6809  smogt  6824  rdglim2  6884  tz7.48lem  6892  tz7.49  6896  swoer  7125  qsss  7157  domtriord  7453  pssnn  7527  ssfi  7529  findcard  7547  findcard2  7548  findcard3  7551  frfi  7553  dffi3  7677  supmo  7698  inf3lem4  7833  carddom2  8143  fidomtri2  8160  pm54.43  8166  infpwfien  8228  alephordi  8240  cardaleph  8255  carduniima  8262  cardinfima  8263  alephval3  8276  dfac5lem4  8292  dfac5  8294  dfac2  8296  kmlem2  8316  cflm  8415  cfslb2n  8433  cfsmolem  8435  isf32lem9  8526  axcc4  8604  domtriomlem  8607  zorn2lem4  8664  zorn2lem6  8666  fpwwe2lem11  8803  fpwwe2lem12  8804  inttsk  8937  inar1  8938  intgru  8977  ingru  8978  indpi  9072  nqpr  9179  ltaddpr  9199  ltexprlem1  9201  ltexprlem5  9205  reclem2pr  9213  reclem4pr  9215  zmulcl  10689  uzm1  10887  uzwo  10913  uzwoOLD  10914  negn0  10937  xmullem2  11224  icoshft  11403  difreicc  11413  fzouzsplit  11580  ssfzoulel  11617  seqf1olem1  11841  seqf1olem2  11842  hashtpg  12182  swrdnd  12322  swrdccatin2  12374  incexclem  13295  sqr2irr  13527  dvds2lem  13541  dvdslelem  13573  divalglem8  13600  euclemma  13790  iserodd  13898  ramcl  14086  mreiincl  14530  joinfval  15167  meetfval  15181  dirge  15403  sylow2alem1  16109  efgredlemb  16236  lbspss  17141  lspsneu  17182  lspsnat  17204  lspsncv0  17205  opsrtoslem2  17542  distop  18559  epttop  18572  isclo2  18651  restdis  18741  subbascn  18817  cnrest2  18849  cnpresti  18851  isnrm2  18921  cmpsublem  18961  cmpcld  18964  dfcon2  18982  t1conperf  18999  1stcrest  19016  lly1stc  19059  uptx  19157  txcn  19158  prdstopn  19160  txcon  19221  cmphaushmeo  19332  fbasrn  19416  csdfil  19426  trufil  19442  fclscf  19557  alexsubALTlem3  19580  alexsubALT  19582  haustsms2  19666  ovoliunlem1  20944  ovoliunnul  20949  volsup2  21044  coeaddlem  21675  plymul0or  21706  radcnv0  21840  wilthlem3  22367  chtub  22510  2sqlem10  22672  pntpbnd1  22794  mptelee  23076  axeuclidlem  23143  axcontlem4  23148  usgrarnedg  23238  usgraedg4  23240  isch3  24579  shmodsi  24727  orthin  24784  h1datomi  24919  stcltr2i  25614  atom1d  25692  sumdmdii  25754  cdj3lem1  25773  disjpreima  25863  suppss3  25962  kerf1hrm  26227  lmxrge0  26318  dmvlsiga  26508  sibfof  26656  erdszelem9  27017  cvmlift2lem1  27121  fundmpss  27506  tfisg  27594  wfisg  27599  frinsg  27635  poseq  27643  sltval2  27726  nodenselem7  27757  nofulllem5  27776  outsideofrflx  28087  mblfinlem3  28355  itg2addnclem3  28370  nn0prpwlem  28442  ivthALT  28455  fnessref  28490  neibastop2lem  28506  tailfb  28523  cover2  28532  fdc  28566  nninfnub  28572  equivtotbnd  28602  prdstotbnd  28618  cntotbnd  28620  ablo4pnp  28670  isdrngo3  28690  crngohomfo  28731  intidl  28754  or32dd  28822  prtlem90  28927  prtlem18  28947  prter2  28951  2reu1  29935  modfsummod  30170  lswn0  30183  frgrancvvdeqlemA  30555  frgrancvvdeqlemC  30557  alrim3con13v  31072  tratrb  31075  onfrALTlem3  31085  onfrALTlem2  31087  onfrALTlem1  31089  trsspwALT2  31387  trsspwALT3  31388  bnj600  31746  bnj1018  31789  bnj1173  31827  bnj1174  31828  bj-axtd  31923  bj-2upleq  32235  lsat0cv  32400  lfl1  32437  lkreqN  32537  atlrelat1  32688  pmaple  33127  pmapsub  33134  pclclN  33257  pclfinN  33266  osumcllem4N  33325  pexmidlem1N  33336  cdleme7ga  33614  lcfl7N  34868
  Copyright terms: Public domain W3C validator