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

Theorem syl6ibr 235
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 211 . 2  |-  ( ch 
->  th )
41, 3syl6 34 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  3imtr4g  278  imp4a  598  nic-ax  1567  nfimd  2011  mo2v  2317  euim  2363  mopick2  2380  2moswap  2387  2eu6  2398  necon3d  2657  necon1d  2658  ralrimd  2804  spcimegf  3140  spcegf  3142  spcimedv  3145  spc2gv  3149  spc3gv  3151  rspcimedv  3164  eqsbc3r  3336  ra4vOLD  3365  ra4OLD  3367  tpid3g  4100  pwpw0  4133  sssn  4143  pwsnALT  4207  ssiun  4334  ssiun2  4335  wefrc  4847  dmcosseq  5115  relssres  5161  restidsing  5180  trin2  5242  ssrnres  5294  sossfld  5302  wfisg  5434  tron  5465  ordtri3or  5474  oneqmini  5493  fnun  5704  f1oun  5856  brprcneu  5881  ssimaex  5953  chfnrn  6016  dffo4  6061  dffo5  6062  tpres  6141  fvclss  6172  isomin  6253  isofrlem  6256  isoselem  6257  fnoprabg  6424  nnsuc  6736  f1oweALT  6804  bropopvvv  6901  bropfvvvvlem  6902  frxp  6933  poxp  6935  fnse  6940  mpt2xopynvov0g  6987  issmo2  7094  smores  7097  smogt  7112  rdglim2  7176  tz7.48lem  7184  tz7.49  7188  swoer  7417  qsss  7450  domtriord  7744  pssnn  7816  ssfi  7818  findcard  7836  findcard2  7837  findcard3  7840  frfi  7842  dffi3  7971  supmo  7992  infmo  8037  inf3lem4  8162  carddom2  8437  fidomtri2  8454  pm54.43  8460  infpwfien  8519  alephordi  8531  cardaleph  8546  carduniima  8553  cardinfima  8554  alephval3  8567  dfac5lem4  8583  dfac5  8585  dfac2  8587  kmlem2  8607  cflm  8706  cfslb2n  8724  cfsmolem  8726  isf32lem9  8817  axcc4  8895  domtriomlem  8898  zorn2lem4  8955  zorn2lem6  8957  fpwwe2lem11  9091  fpwwe2lem12  9092  inttsk  9225  inar1  9226  intgru  9265  ingru  9266  indpi  9358  nqpr  9465  ltaddpr  9485  ltexprlem1  9487  ltexprlem5  9491  reclem2pr  9499  reclem4pr  9501  negn0  10076  zmulcl  11014  uzm1  11218  uzwo  11251  xmullem2  11580  icoshft  11783  difreicc  11793  fzouzsplit  11984  ssfzoulel  12036  seqf1olem1  12284  seqf1olem2  12285  hashge2el2difr  12671  hashtpg  12674  swrdccatin2  12880  modfsummod  13903  incexclem  13943  sqrt2irr  14350  dvds2lem  14364  dvdslelem  14398  divalglem8  14429  euclemma  14714  iserodd  14834  ramcl  15036  mreiincl  15551  joinfval  16296  meetfval  16310  dirge  16532  sylow2alem1  17318  efgredlemb  17445  kerf1hrm  18020  lbspss  18354  lspsneu  18395  lspsnat  18417  lspsncv0  18418  opsrtoslem2  18757  distop  20060  epttop  20073  isclo2  20153  restdis  20243  subbascn  20319  cnrest2  20351  cnpresti  20353  isnrm2  20423  cmpsublem  20463  cmpcld  20466  dfcon2  20483  t1conperf  20500  1stcrest  20517  lly1stc  20560  uptx  20689  txcn  20690  prdstopn  20692  txcon  20753  cmphaushmeo  20864  fbasrn  20948  csdfil  20958  trufil  20974  fclscf  21089  alexsubALTlem3  21113  alexsubALT  21115  haustsms2  21200  ovoliunlem1  22504  ovoliunnul  22509  volsup2  22612  coeaddlem  23252  plymul0or  23283  radcnv0  23420  wilthlem3  24044  chtub  24189  2sqlem10  24351  pntpbnd1  24473  mptelee  24974  axeuclidlem  25041  axcontlem4  25046  usgrarnedg  25160  usgraedg4  25163  frgrancvvdeqlemA  25814  frgrancvvdeqlemC  25816  isch3  26943  shmodsi  27091  orthin  27148  h1datomi  27283  stcltr2i  27977  atom1d  28055  sumdmdii  28117  cdj3lem1  28136  disjpreima  28243  lmxrge0  28807  dmvlsiga  29000  sibfof  29222  bnj600  29779  bnj1018  29822  bnj1173  29860  bnj1174  29861  erdszelem9  29971  cvmlift2lem1  30074  fundmpss  30456  tfisg  30506  frinsg  30532  poseq  30540  sltval2  30592  nodenselem7  30625  nofulllem5  30644  outsideofrflx  30943  nn0prpwlem  31027  ivthALT  31040  fnessref  31062  neibastop2lem  31065  tailfb  31082  bj-axtd  31222  bj-ssbequ1  31302  bj-nfdt0  31333  bj-2upleq  31651  icorempt2  31799  isbasisrelowllem2  31804  poimirlem3  31988  poimirlem4  31989  poimirlem29  32014  mblfinlem3  32024  itg2addnclem3  32040  cover2  32085  fdc  32119  nninfnub  32125  equivtotbnd  32155  prdstotbnd  32171  cntotbnd  32173  ablo4pnp  32223  isdrngo3  32243  crngohomfo  32284  intidl  32307  or32dd  32375  prtlem90  32476  prtlem18  32494  prter2  32498  lsat0cv  32644  lfl1  32681  lkreqN  32781  atlrelat1  32932  pmaple  33371  pmapsub  33378  pclclN  33501  pclfinN  33510  osumcllem4N  33569  pexmidlem1N  33580  cdleme7ga  33859  lcfl7N  35114  ss2iundf  36296  brtrclfv2  36364  nzss  36710  3impexpbicom  36878  alrim3con13v  36938  tratrb  36941  onfrALTlem3  36954  onfrALTlem2  36956  onfrALTlem1  36958  trsspwALT2  37247  trsspwALT3  37248  2reu1  38645  elmod2OLD  38764  bgoldbwt  38916  bgoldbst  38917  sgoldbalt  38920  lswn0  38960  uhgrissubgr  39397  nbgrnself2  39481  pthdivtx  39762  usgedgimp  39988  usgedgimpALT  39991  2zrngamgm  40212  fldivexpfllog2  40649
  Copyright terms: Public domain W3C validator