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, 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 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  589  nic-ax  1493  nfimd  1903  mo2v  2275  mo2vOLD  2276  mo2vOLDOLD  2277  euim  2330  mopick2  2348  2moswap  2355  2eu1OLD  2363  2eu6  2369  necon3adOLD  2654  necon3d  2667  necon1d  2668  ralrimd  2847  spcimegf  3174  spcegf  3176  spcimedv  3179  spc2gv  3183  spc3gv  3185  rspcimedv  3198  eqsbc3r  3375  ra4vOLD  3410  ra4OLD  3412  tpid3g  4130  pwpw0  4163  sssn  4173  pwsnALT  4229  ssiun  4357  ssiun2  4358  reusv6OLD  4648  wefrc  4863  tron  4891  ordtri3or  4900  oneqmini  4919  dmcosseq  5254  relssres  5301  restidsing  5320  trin2  5380  ssrnres  5435  sossfld  5444  fnun  5677  f1oun  5825  brprcneu  5849  ssimaex  5923  chfnrn  5983  dffo4  6032  dffo5  6033  fvclss  6139  isomin  6218  isofrlem  6221  isoselem  6222  fnoprabg  6388  nnsuc  6702  f1oweALT  6769  bropopvvv  6865  frxp  6895  poxp  6897  fnse  6902  mpt2xopynvov0g  6944  issmo2  7022  smores  7025  smogt  7040  rdglim2  7100  tz7.48lem  7108  tz7.49  7112  swoer  7341  qsss  7374  domtriord  7665  pssnn  7740  ssfi  7742  findcard  7761  findcard2  7762  findcard3  7765  frfi  7767  dffi3  7893  supmo  7914  inf3lem4  8051  carddom2  8361  fidomtri2  8378  pm54.43  8384  infpwfien  8446  alephordi  8458  cardaleph  8473  carduniima  8480  cardinfima  8481  alephval3  8494  dfac5lem4  8510  dfac5  8512  dfac2  8514  kmlem2  8534  cflm  8633  cfslb2n  8651  cfsmolem  8653  isf32lem9  8744  axcc4  8822  domtriomlem  8825  zorn2lem4  8882  zorn2lem6  8884  fpwwe2lem11  9021  fpwwe2lem12  9022  inttsk  9155  inar1  9156  intgru  9195  ingru  9196  indpi  9288  nqpr  9395  ltaddpr  9415  ltexprlem1  9417  ltexprlem5  9421  reclem2pr  9429  reclem4pr  9431  zmulcl  10919  uzm1  11122  uzwo  11155  uzwoOLD  11156  negn0  11179  xmullem2  11468  icoshft  11653  difreicc  11663  fzouzsplit  11842  ssfzoulel  11888  seqf1olem1  12128  seqf1olem2  12129  hashtpg  12505  swrdnd  12639  swrdccatin2  12694  modfsummod  13590  incexclem  13630  sqrt2irr  13964  dvds2lem  13978  dvdslelem  14012  divalglem8  14040  euclemma  14231  iserodd  14341  ramcl  14529  mreiincl  14975  joinfval  15610  meetfval  15624  dirge  15846  sylow2alem1  16616  efgredlemb  16743  kerf1hrm  17371  lbspss  17707  lspsneu  17748  lspsnat  17770  lspsncv0  17771  opsrtoslem2  18128  distop  19475  epttop  19488  isclo2  19567  restdis  19657  subbascn  19733  cnrest2  19765  cnpresti  19767  isnrm2  19837  cmpsublem  19877  cmpcld  19880  dfcon2  19898  t1conperf  19915  1stcrest  19932  lly1stc  19975  uptx  20104  txcn  20105  prdstopn  20107  txcon  20168  cmphaushmeo  20279  fbasrn  20363  csdfil  20373  trufil  20389  fclscf  20504  alexsubALTlem3  20527  alexsubALT  20529  haustsms2  20613  ovoliunlem1  21891  ovoliunnul  21896  volsup2  21992  coeaddlem  22624  plymul0or  22655  radcnv0  22789  wilthlem3  23322  chtub  23465  2sqlem10  23627  pntpbnd1  23749  mptelee  24176  axeuclidlem  24243  axcontlem4  24248  usgrarnedg  24362  usgraedg4  24365  frgrancvvdeqlemA  25015  frgrancvvdeqlemC  25017  isch3  26137  shmodsi  26285  orthin  26342  h1datomi  26477  stcltr2i  27172  atom1d  27250  sumdmdii  27312  cdj3lem1  27331  disjpreima  27423  lmxrge0  27912  dmvlsiga  28107  sibfof  28260  erdszelem9  28621  cvmlift2lem1  28725  fundmpss  29172  tfisg  29260  wfisg  29265  frinsg  29301  poseq  29309  sltval2  29392  nodenselem7  29423  nofulllem5  29442  outsideofrflx  29753  mblfinlem3  30029  itg2addnclem3  30044  nn0prpwlem  30116  ivthALT  30129  fnessref  30151  neibastop2lem  30154  tailfb  30171  cover2  30180  fdc  30214  nninfnub  30220  equivtotbnd  30250  prdstotbnd  30266  cntotbnd  30268  ablo4pnp  30318  isdrngo3  30338  crngohomfo  30379  intidl  30402  or32dd  30470  prtlem90  30574  prtlem18  30594  prter2  30598  nzss  31198  2reu1  32145  lswn0  32297  usgedgimp  32357  usgedgimpALT  32360  tpres  32506  2zrngamgm  32572  3impexpbicom  33089  alrim3con13v  33172  tratrb  33175  onfrALTlem3  33184  onfrALTlem2  33186  onfrALTlem1  33188  trsspwALT2  33485  trsspwALT3  33486  bnj600  33845  bnj1018  33888  bnj1173  33926  bnj1174  33927  bj-axtd  34065  bj-nfdt0  34131  bj-2upleq  34453  lsat0cv  34633  lfl1  34670  lkreqN  34770  atlrelat1  34921  pmaple  35360  pmapsub  35367  pclclN  35490  pclfinN  35499  osumcllem4N  35558  pexmidlem1N  35569  cdleme7ga  35848  lcfl7N  37103
  Copyright terms: Public domain W3C validator