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  1480  nfimd  1850  mo2v  2260  mo2vOLD  2261  mo2vOLDOLD  2262  euim  2324  mopick2  2348  2moswap  2356  2eu1OLD  2365  2eu6  2371  necon3ad  2659  necon3d  2661  necon1d  2695  ralrimd  2819  spcimegf  3066  spcegf  3068  spcimedv  3071  spc2gv  3075  spc3gv  3077  rspcimedv  3090  eqsbc3r  3263  ra4  3297  tpid3g  4005  pwpw0  4036  sssn  4046  pwsnALT  4101  ssiun  4227  ssiun2  4228  reusv6OLD  4518  wefrc  4729  tron  4757  ordtri3or  4766  oneqmini  4785  dmcosseq  5116  relssres  5162  restidsing  5177  trin2  5236  ssrnres  5291  sossfld  5300  fnun  5532  f1oun  5675  brprcneu  5699  ssimaex  5771  chfnrn  5829  dffo4  5874  dffo5  5875  fvclss  5974  isomin  6043  isofrlem  6046  isoselem  6047  fnoprabg  6206  nnsuc  6508  f1oweALT  6576  bropopvvv  6668  frxp  6697  poxp  6699  fnse  6704  mpt2xopynvov0g  6746  issmo2  6825  smores  6828  smogt  6843  rdglim2  6903  tz7.48lem  6911  tz7.49  6915  swoer  7144  qsss  7176  domtriord  7472  pssnn  7546  ssfi  7548  findcard  7566  findcard2  7567  findcard3  7570  frfi  7572  dffi3  7696  supmo  7717  inf3lem4  7852  carddom2  8162  fidomtri2  8179  pm54.43  8185  infpwfien  8247  alephordi  8259  cardaleph  8274  carduniima  8281  cardinfima  8282  alephval3  8295  dfac5lem4  8311  dfac5  8313  dfac2  8315  kmlem2  8335  cflm  8434  cfslb2n  8452  cfsmolem  8454  isf32lem9  8545  axcc4  8623  domtriomlem  8626  zorn2lem4  8683  zorn2lem6  8685  fpwwe2lem11  8822  fpwwe2lem12  8823  inttsk  8956  inar1  8957  intgru  8996  ingru  8997  indpi  9091  nqpr  9198  ltaddpr  9218  ltexprlem1  9220  ltexprlem5  9224  reclem2pr  9232  reclem4pr  9234  zmulcl  10708  uzm1  10906  uzwo  10932  uzwoOLD  10933  negn0  10956  xmullem2  11243  icoshft  11422  difreicc  11432  fzouzsplit  11599  ssfzoulel  11636  seqf1olem1  11860  seqf1olem2  11861  hashtpg  12201  swrdnd  12341  swrdccatin2  12393  incexclem  13314  sqr2irr  13546  dvds2lem  13560  dvdslelem  13592  divalglem8  13619  euclemma  13809  iserodd  13917  ramcl  14105  mreiincl  14549  joinfval  15186  meetfval  15200  dirge  15422  sylow2alem1  16131  efgredlemb  16258  kerf1hrm  16846  lbspss  17178  lspsneu  17219  lspsnat  17241  lspsncv0  17242  opsrtoslem2  17581  distop  18615  epttop  18628  isclo2  18707  restdis  18797  subbascn  18873  cnrest2  18905  cnpresti  18907  isnrm2  18977  cmpsublem  19017  cmpcld  19020  dfcon2  19038  t1conperf  19055  1stcrest  19072  lly1stc  19115  uptx  19213  txcn  19214  prdstopn  19216  txcon  19277  cmphaushmeo  19388  fbasrn  19472  csdfil  19482  trufil  19498  fclscf  19613  alexsubALTlem3  19636  alexsubALT  19638  haustsms2  19722  ovoliunlem1  21000  ovoliunnul  21005  volsup2  21100  coeaddlem  21731  plymul0or  21762  radcnv0  21896  wilthlem3  22423  chtub  22566  2sqlem10  22728  pntpbnd1  22850  mptelee  23156  axeuclidlem  23223  axcontlem4  23228  usgrarnedg  23318  usgraedg4  23320  isch3  24659  shmodsi  24807  orthin  24864  h1datomi  24999  stcltr2i  25694  atom1d  25772  sumdmdii  25834  cdj3lem1  25853  disjpreima  25943  suppss3  26042  lmxrge0  26397  dmvlsiga  26587  sibfof  26741  erdszelem9  27102  cvmlift2lem1  27206  fundmpss  27592  tfisg  27680  wfisg  27685  frinsg  27721  poseq  27729  sltval2  27812  nodenselem7  27843  nofulllem5  27862  outsideofrflx  28173  mblfinlem3  28449  itg2addnclem3  28464  nn0prpwlem  28536  ivthALT  28549  fnessref  28584  neibastop2lem  28600  tailfb  28617  cover2  28626  fdc  28660  nninfnub  28666  equivtotbnd  28696  prdstotbnd  28712  cntotbnd  28714  ablo4pnp  28764  isdrngo3  28784  crngohomfo  28825  intidl  28848  or32dd  28916  prtlem90  29021  prtlem18  29041  prter2  29045  2reu1  30029  modfsummod  30264  lswn0  30277  frgrancvvdeqlemA  30649  frgrancvvdeqlemC  30651  3impexpbicom  31175  alrim3con13v  31258  tratrb  31261  onfrALTlem3  31271  onfrALTlem2  31273  onfrALTlem1  31275  trsspwALT2  31572  trsspwALT3  31573  bnj600  31931  bnj1018  31974  bnj1173  32012  bnj1174  32013  bj-axtd  32148  bj-nfdt0  32203  bj-2upleq  32524  lsat0cv  32697  lfl1  32734  lkreqN  32834  atlrelat1  32985  pmaple  33424  pmapsub  33431  pclclN  33554  pclfinN  33563  osumcllem4N  33622  pexmidlem1N  33633  cdleme7ga  33911  lcfl7N  35165
  Copyright terms: Public domain W3C validator