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  587  nic-ax  1513  nfimd  1925  mo2v  2225  mo2vOLD  2226  mo2vOLDOLD  2227  euim  2275  mopick2  2293  2moswap  2300  2eu1OLD  2308  2eu6  2314  necon3adOLD  2593  necon3d  2606  necon1d  2607  ralrimd  2786  spcimegf  3113  spcegf  3115  spcimedv  3118  spc2gv  3122  spc3gv  3124  rspcimedv  3137  eqsbc3r  3309  ra4vOLD  3338  ra4OLD  3340  tpid3g  4059  pwpw0  4092  sssn  4102  pwsnALT  4158  ssiun  4285  ssiun2  4286  wefrc  4787  tron  4815  ordtri3or  4824  oneqmini  4843  dmcosseq  5177  relssres  5223  restidsing  5242  trin2  5303  ssrnres  5355  sossfld  5363  fnun  5595  f1oun  5743  brprcneu  5767  ssimaex  5839  chfnrn  5900  dffo4  5949  dffo5  5950  tpres  6026  fvclss  6055  isomin  6134  isofrlem  6137  isoselem  6138  fnoprabg  6302  nnsuc  6616  f1oweALT  6683  bropopvvv  6779  frxp  6809  poxp  6811  fnse  6816  mpt2xopynvov0g  6860  issmo2  6938  smores  6941  smogt  6956  rdglim2  7016  tz7.48lem  7024  tz7.49  7028  swoer  7257  qsss  7290  domtriord  7582  pssnn  7654  ssfi  7656  findcard  7674  findcard2  7675  findcard3  7678  frfi  7680  dffi3  7806  supmo  7826  inf3lem4  7962  carddom2  8271  fidomtri2  8288  pm54.43  8294  infpwfien  8356  alephordi  8368  cardaleph  8383  carduniima  8390  cardinfima  8391  alephval3  8404  dfac5lem4  8420  dfac5  8422  dfac2  8424  kmlem2  8444  cflm  8543  cfslb2n  8561  cfsmolem  8563  isf32lem9  8654  axcc4  8732  domtriomlem  8735  zorn2lem4  8792  zorn2lem6  8794  fpwwe2lem11  8929  fpwwe2lem12  8930  inttsk  9063  inar1  9064  intgru  9103  ingru  9104  indpi  9196  nqpr  9303  ltaddpr  9323  ltexprlem1  9325  ltexprlem5  9329  reclem2pr  9337  reclem4pr  9339  zmulcl  10829  uzm1  11031  uzwo  11064  negn0  11087  xmullem2  11378  icoshft  11563  difreicc  11573  fzouzsplit  11755  ssfzoulel  11805  seqf1olem1  12049  seqf1olem2  12050  hashtpg  12427  swrdccatin2  12623  modfsummod  13610  incexclem  13650  sqrt2irr  13984  dvds2lem  13998  dvdslelem  14032  divalglem8  14060  euclemma  14251  iserodd  14361  ramcl  14549  mreiincl  15003  joinfval  15748  meetfval  15762  dirge  15984  sylow2alem1  16754  efgredlemb  16881  kerf1hrm  17505  lbspss  17841  lspsneu  17882  lspsnat  17904  lspsncv0  17905  opsrtoslem2  18262  distop  19582  epttop  19595  isclo2  19675  restdis  19765  subbascn  19841  cnrest2  19873  cnpresti  19875  isnrm2  19945  cmpsublem  19985  cmpcld  19988  dfcon2  20005  t1conperf  20022  1stcrest  20039  lly1stc  20082  uptx  20211  txcn  20212  prdstopn  20214  txcon  20275  cmphaushmeo  20386  fbasrn  20470  csdfil  20480  trufil  20496  fclscf  20611  alexsubALTlem3  20634  alexsubALT  20636  haustsms2  20720  ovoliunlem1  21998  ovoliunnul  22003  volsup2  22099  coeaddlem  22731  plymul0or  22762  radcnv0  22896  wilthlem3  23461  chtub  23604  2sqlem10  23766  pntpbnd1  23888  mptelee  24319  axeuclidlem  24386  axcontlem4  24391  usgrarnedg  24505  usgraedg4  24508  frgrancvvdeqlemA  25158  frgrancvvdeqlemC  25160  isch3  26276  shmodsi  26424  orthin  26481  h1datomi  26616  stcltr2i  27310  atom1d  27388  sumdmdii  27450  cdj3lem1  27469  disjpreima  27574  lmxrge0  28088  dmvlsiga  28278  sibfof  28465  erdszelem9  28832  cvmlift2lem1  28936  fundmpss  29362  tfisg  29449  wfisg  29454  frinsg  29490  poseq  29498  sltval2  29581  nodenselem7  29612  nofulllem5  29631  outsideofrflx  29930  mblfinlem3  30218  itg2addnclem3  30234  nn0prpwlem  30306  ivthALT  30319  fnessref  30341  neibastop2lem  30344  tailfb  30361  cover2  30370  fdc  30404  nninfnub  30410  equivtotbnd  30440  prdstotbnd  30456  cntotbnd  30458  ablo4pnp  30508  isdrngo3  30528  crngohomfo  30569  intidl  30592  or32dd  30660  prtlem90  30764  prtlem18  30784  prter2  30788  nzss  31390  2reu1  32357  elmod2OLD  32463  lswn0  32554  usgedgimp  32721  usgedgimpALT  32724  2zrngamgm  32945  fldivexpfllog2  33386  3impexpbicom  33554  alrim3con13v  33640  tratrb  33643  onfrALTlem3  33656  onfrALTlem2  33658  onfrALTlem1  33660  trsspwALT2  33957  trsspwALT3  33958  bnj600  34324  bnj1018  34367  bnj1173  34405  bnj1174  34406  bj-axtd  34529  bj-nfdt0  34595  bj-2upleq  34918  lsat0cv  35171  lfl1  35208  lkreqN  35308  atlrelat1  35459  pmaple  35898  pmapsub  35905  pclclN  36028  pclfinN  36037  osumcllem4N  36096  pexmidlem1N  36107  cdleme7ga  36386  lcfl7N  37641  brtrclfv2  38258
  Copyright terms: Public domain W3C validator