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

Theorem syl6ibr 230
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  |-  ( 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 209 . 2  |-  ( ch 
->  th )
41, 3syl6 34 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  3imtr4g  273  imp4a  592  nic-ax  1550  nfimd  1977  mo2v  2278  euim  2324  mopick2  2341  2moswap  2348  2eu6  2359  necon3d  2617  necon1d  2618  ralrimd  2764  spcimegf  3098  spcegf  3100  spcimedv  3103  spc2gv  3107  spc3gv  3109  rspcimedv  3122  eqsbc3r  3294  ra4vOLD  3323  ra4OLD  3325  tpid3g  4053  pwpw0  4086  sssn  4096  pwsnALT  4152  ssiun  4279  ssiun2  4280  wefrc  4785  dmcosseq  5053  relssres  5099  restidsing  5118  trin2  5180  ssrnres  5232  sossfld  5240  wfisg  5372  tron  5403  ordtri3or  5412  oneqmini  5431  fnun  5638  f1oun  5788  brprcneu  5813  ssimaex  5885  chfnrn  5947  dffo4  5992  dffo5  5993  tpres  6071  fvclss  6101  isomin  6182  isofrlem  6185  isoselem  6186  fnoprabg  6350  nnsuc  6662  f1oweALT  6730  bropopvvv  6826  frxp  6856  poxp  6858  fnse  6863  mpt2xopynvov0g  6910  issmo2  7018  smores  7021  smogt  7036  rdglim2  7100  tz7.48lem  7108  tz7.49  7112  swoer  7341  qsss  7374  domtriord  7666  pssnn  7738  ssfi  7740  findcard  7758  findcard2  7759  findcard3  7762  frfi  7764  dffi3  7893  supmo  7914  infmo  7959  inf3lem4  8084  carddom2  8358  fidomtri2  8375  pm54.43  8381  infpwfien  8439  alephordi  8451  cardaleph  8466  carduniima  8473  cardinfima  8474  alephval3  8487  dfac5lem4  8503  dfac5  8505  dfac2  8507  kmlem2  8527  cflm  8626  cfslb2n  8644  cfsmolem  8646  isf32lem9  8737  axcc4  8815  domtriomlem  8818  zorn2lem4  8875  zorn2lem6  8877  fpwwe2lem11  9011  fpwwe2lem12  9012  inttsk  9145  inar1  9146  intgru  9185  ingru  9186  indpi  9278  nqpr  9385  ltaddpr  9405  ltexprlem1  9407  ltexprlem5  9411  reclem2pr  9419  reclem4pr  9421  negn0  9994  zmulcl  10931  uzm1  11135  uzwo  11168  xmullem2  11497  icoshft  11700  difreicc  11710  fzouzsplit  11899  ssfzoulel  11950  seqf1olem1  12197  seqf1olem2  12198  hashge2el2difr  12581  hashtpg  12584  swrdccatin2  12784  modfsummod  13792  incexclem  13832  sqrt2irr  14239  dvds2lem  14253  dvdslelem  14287  divalglem8  14318  euclemma  14603  iserodd  14723  ramcl  14925  mreiincl  15440  joinfval  16185  meetfval  16199  dirge  16421  sylow2alem1  17207  efgredlemb  17334  kerf1hrm  17909  lbspss  18243  lspsneu  18284  lspsnat  18306  lspsncv0  18307  opsrtoslem2  18646  distop  19948  epttop  19961  isclo2  20041  restdis  20131  subbascn  20207  cnrest2  20239  cnpresti  20241  isnrm2  20311  cmpsublem  20351  cmpcld  20354  dfcon2  20371  t1conperf  20388  1stcrest  20405  lly1stc  20448  uptx  20577  txcn  20578  prdstopn  20580  txcon  20641  cmphaushmeo  20752  fbasrn  20836  csdfil  20846  trufil  20862  fclscf  20977  alexsubALTlem3  21001  alexsubALT  21003  haustsms2  21088  ovoliunlem1  22392  ovoliunnul  22397  volsup2  22500  coeaddlem  23140  plymul0or  23171  radcnv0  23308  wilthlem3  23932  chtub  24077  2sqlem10  24239  pntpbnd1  24361  mptelee  24862  axeuclidlem  24929  axcontlem4  24934  usgrarnedg  25048  usgraedg4  25051  frgrancvvdeqlemA  25702  frgrancvvdeqlemC  25704  isch3  26831  shmodsi  26979  orthin  27036  h1datomi  27171  stcltr2i  27865  atom1d  27943  sumdmdii  28005  cdj3lem1  28024  disjpreima  28135  lmxrge0  28705  dmvlsiga  28898  sibfof  29120  bnj600  29677  bnj1018  29720  bnj1173  29758  bnj1174  29759  erdszelem9  29869  cvmlift2lem1  29972  fundmpss  30353  tfisg  30403  frinsg  30429  poseq  30437  sltval2  30489  nodenselem7  30520  nofulllem5  30539  outsideofrflx  30838  nn0prpwlem  30922  ivthALT  30935  fnessref  30957  neibastop2lem  30960  tailfb  30977  bj-axtd  31120  bj-nfdt0  31189  bj-2upleq  31517  icorempt2  31661  isbasisrelowllem2  31666  poimirlem3  31850  poimirlem4  31851  poimirlem29  31876  mblfinlem3  31886  itg2addnclem3  31902  cover2  31947  fdc  31981  nninfnub  31987  equivtotbnd  32017  prdstotbnd  32033  cntotbnd  32035  ablo4pnp  32085  isdrngo3  32105  crngohomfo  32146  intidl  32169  or32dd  32237  prtlem90  32340  prtlem18  32360  prter2  32364  lsat0cv  32511  lfl1  32548  lkreqN  32648  atlrelat1  32799  pmaple  33238  pmapsub  33245  pclclN  33368  pclfinN  33377  osumcllem4N  33436  pexmidlem1N  33447  cdleme7ga  33726  lcfl7N  34981  ss2iundf  36164  brtrclfv2  36232  nzss  36579  3impexpbicom  36747  alrim3con13v  36807  tratrb  36810  onfrALTlem3  36823  onfrALTlem2  36825  onfrALTlem1  36827  trsspwALT2  37123  trsspwALT3  37124  2reu1  38421  elmod2OLD  38539  bgoldbwt  38691  bgoldbst  38692  sgoldbalt  38695  lswn0  38733  uhgrissubgr  39084  nbgrnself2  39167  usgedgimp  39306  usgedgimpALT  39309  2zrngamgm  39530  fldivexpfllog2  39969
  Copyright terms: Public domain W3C validator