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  1552  nfimd  1975  mo2v  2273  mo2vOLD  2274  mo2vOLDOLD  2275  euim  2322  mopick2  2340  2moswap  2347  2eu1OLD  2355  2eu6  2361  necon3adOLD  2642  necon3d  2655  necon1d  2656  ralrimd  2836  spcimegf  3166  spcegf  3168  spcimedv  3171  spc2gv  3175  spc3gv  3177  rspcimedv  3190  eqsbc3r  3362  ra4vOLD  3391  ra4OLD  3393  tpid3g  4118  pwpw0  4151  sssn  4161  pwsnALT  4217  ssiun  4344  ssiun2  4345  wefrc  4848  dmcosseq  5116  relssres  5162  restidsing  5181  trin2  5243  ssrnres  5295  sossfld  5303  wfisg  5434  tron  5465  ordtri3or  5474  oneqmini  5493  fnun  5700  f1oun  5850  brprcneu  5874  ssimaex  5946  chfnrn  6008  dffo4  6053  dffo5  6054  tpres  6132  fvclss  6162  isomin  6243  isofrlem  6246  isoselem  6247  fnoprabg  6411  nnsuc  6723  f1oweALT  6791  bropopvvv  6887  frxp  6917  poxp  6919  fnse  6924  mpt2xopynvov0g  6968  issmo2  7076  smores  7079  smogt  7094  rdglim2  7158  tz7.48lem  7166  tz7.49  7170  swoer  7399  qsss  7432  domtriord  7724  pssnn  7796  ssfi  7798  findcard  7816  findcard2  7817  findcard3  7820  frfi  7822  dffi3  7951  supmo  7972  inf3lem4  8136  carddom2  8410  fidomtri2  8427  pm54.43  8433  infpwfien  8491  alephordi  8503  cardaleph  8518  carduniima  8525  cardinfima  8526  alephval3  8539  dfac5lem4  8555  dfac5  8557  dfac2  8559  kmlem2  8579  cflm  8678  cfslb2n  8696  cfsmolem  8698  isf32lem9  8789  axcc4  8867  domtriomlem  8870  zorn2lem4  8927  zorn2lem6  8929  fpwwe2lem11  9064  fpwwe2lem12  9065  inttsk  9198  inar1  9199  intgru  9238  ingru  9239  indpi  9331  nqpr  9438  ltaddpr  9458  ltexprlem1  9460  ltexprlem5  9464  reclem2pr  9472  reclem4pr  9474  negn0  10047  zmulcl  10985  uzm1  11189  uzwo  11222  xmullem2  11551  icoshft  11752  difreicc  11762  fzouzsplit  11951  ssfzoulel  12002  seqf1olem1  12249  seqf1olem2  12250  hashtpg  12632  swrdccatin2  12828  modfsummod  13832  incexclem  13872  sqrt2irr  14279  dvds2lem  14293  dvdslelem  14327  divalglem8  14356  euclemma  14627  iserodd  14739  ramcl  14941  mreiincl  15444  joinfval  16189  meetfval  16203  dirge  16425  sylow2alem1  17195  efgredlemb  17322  kerf1hrm  17897  lbspss  18231  lspsneu  18272  lspsnat  18294  lspsncv0  18295  opsrtoslem2  18634  distop  19933  epttop  19946  isclo2  20026  restdis  20116  subbascn  20192  cnrest2  20224  cnpresti  20226  isnrm2  20296  cmpsublem  20336  cmpcld  20339  dfcon2  20356  t1conperf  20373  1stcrest  20390  lly1stc  20433  uptx  20562  txcn  20563  prdstopn  20565  txcon  20626  cmphaushmeo  20737  fbasrn  20821  csdfil  20831  trufil  20847  fclscf  20962  alexsubALTlem3  20986  alexsubALT  20988  haustsms2  21073  ovoliunlem1  22324  ovoliunnul  22329  volsup2  22431  coeaddlem  23062  plymul0or  23093  radcnv0  23227  wilthlem3  23851  chtub  23994  2sqlem10  24156  pntpbnd1  24278  mptelee  24762  axeuclidlem  24829  axcontlem4  24834  usgrarnedg  24948  usgraedg4  24951  frgrancvvdeqlemA  25601  frgrancvvdeqlemC  25603  isch3  26720  shmodsi  26868  orthin  26925  h1datomi  27060  stcltr2i  27754  atom1d  27832  sumdmdii  27894  cdj3lem1  27913  disjpreima  28024  lmxrge0  28588  dmvlsiga  28781  sibfof  28992  bnj600  29509  bnj1018  29552  bnj1173  29590  bnj1174  29591  erdszelem9  29701  cvmlift2lem1  29804  fundmpss  30185  tfisg  30235  frinsg  30261  poseq  30269  sltval2  30321  nodenselem7  30352  nofulllem5  30371  outsideofrflx  30670  nn0prpwlem  30754  ivthALT  30767  fnessref  30789  neibastop2lem  30792  tailfb  30809  bj-axtd  30952  bj-nfdt0  31019  bj-2upleq  31346  icorempt2  31479  isbasisrelowllem2  31484  poimirlem3  31637  poimirlem4  31638  poimirlem29  31663  mblfinlem3  31673  itg2addnclem3  31689  cover2  31734  fdc  31768  nninfnub  31774  equivtotbnd  31804  prdstotbnd  31820  cntotbnd  31822  ablo4pnp  31872  isdrngo3  31892  crngohomfo  31933  intidl  31956  or32dd  32024  prtlem90  32127  prtlem18  32147  prter2  32151  lsat0cv  32298  lfl1  32335  lkreqN  32435  atlrelat1  32586  pmaple  33025  pmapsub  33032  pclclN  33155  pclfinN  33164  osumcllem4N  33223  pexmidlem1N  33234  cdleme7ga  33513  lcfl7N  34768  ss2iundf  35880  brtrclfv2  35948  nzss  36293  3impexpbicom  36461  alrim3con13v  36521  tratrb  36524  onfrALTlem3  36537  onfrALTlem2  36539  onfrALTlem1  36541  trsspwALT2  36837  trsspwALT3  36838  2reu1  37988  elmod2OLD  38106  bgoldbwt  38258  bgoldbst  38259  sgoldbalt  38262  lswn0  38300  usgedgimp  38463  usgedgimpALT  38466  2zrngamgm  38687  fldivexpfllog2  39127
  Copyright terms: Public domain W3C validator