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

Theorem syl6ibr 219
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-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 198 . 2  |-  ( ch 
->  th )
41, 3syl6 31 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr4g  262  imp4a  573  3impexpbicom  1376  nic-ax  1447  nfimd  1827  equs5eOLD  1911  ax12olem2  2006  ax12olem2OLD  2012  euim  2330  mopick2  2347  2moswap  2355  2eu1  2360  necon3ad  2634  necon3d  2636  necon1d  2667  ralrimd  2786  spcimegf  3022  spcegf  3024  spcimedv  3027  spc2gv  3031  spc3gv  3033  rspcimedv  3046  eqsbc3r  3210  ra5  3237  tpid3g  3911  pwpw0  3938  sssn  3949  pwsnALT  4002  ssiun  4125  ssiun2  4126  wefrc  4568  tron  4596  ordtri3or  4605  oneqmini  4624  reusv6OLD  4726  nnsuc  4854  dmcosseq  5129  relssres  5175  trin2  5249  ssrnres  5301  sossfld  5309  fnun  5543  f1oun  5686  brprcneu  5713  ssimaex  5780  chfnrn  5833  dffo4  5877  dffo5  5878  fvclss  5972  isomin  6049  isofrlem  6052  isoselem  6053  f1oweALT  6066  fnoprabg  6163  bropopvvv  6418  frxp  6448  poxp  6450  fnse  6455  mpt2xopynvov0g  6457  issmo2  6603  smores  6606  smogt  6621  rdglim2  6682  tz7.48lem  6690  tz7.49  6694  swoer  6925  qsss  6957  domtriord  7245  pssnn  7319  ssfi  7321  findcard  7339  findcard2  7340  findcard3  7342  frfi  7344  dffi3  7428  supmo  7449  inf3lem4  7578  carddom2  7856  fidomtri2  7873  pm54.43  7879  infpwfien  7935  alephordi  7947  cardaleph  7962  carduniima  7969  cardinfima  7970  alephval3  7983  dfac5lem4  7999  dfac5  8001  dfac2  8003  kmlem2  8023  cflm  8122  cfslb2n  8140  cfsmolem  8142  isf32lem9  8233  axcc4  8311  domtriomlem  8314  zorn2lem4  8371  zorn2lem6  8373  fpwwe2lem11  8507  fpwwe2lem12  8508  inttsk  8641  inar1  8642  intgru  8681  ingru  8682  indpi  8776  nqpr  8883  ltaddpr  8903  ltexprlem1  8905  ltexprlem5  8909  reclem2pr  8917  reclem4pr  8919  zmulcl  10316  uzm1  10508  uzwo  10531  uzwoOLD  10532  negn0  10554  xmullem2  10836  icoshft  11011  difreicc  11020  fzouzsplit  11160  seqf1olem1  11354  seqf1olem2  11355  hashtpg  11683  incexclem  12608  sqr2irr  12840  dvds2lem  12854  dvdslelem  12886  divalglem8  12912  euclemma  13100  iserodd  13201  ramcl  13389  mreiincl  13813  dirge  14674  sylow2alem1  15243  efgredlemb  15370  lbspss  16146  lspsneu  16187  lspsnat  16209  lspsncv0  16210  opsrtoslem2  16537  distop  17052  epttop  17065  isclo2  17144  restdis  17234  subbascn  17310  cnrest2  17342  cnpresti  17344  isnrm2  17414  cmpsublem  17454  cmpcld  17457  dfcon2  17474  t1conperf  17491  1stcrest  17508  lly1stc  17551  uptx  17649  txcn  17650  prdstopn  17652  txcon  17713  cmphaushmeo  17824  fbasrn  17908  csdfil  17918  trufil  17934  fclscf  18049  alexsubALTlem3  18072  alexsubALT  18074  haustsms2  18158  ovoliunlem1  19390  ovoliunnul  19395  volsup2  19489  coeaddlem  20159  plymul0or  20190  radcnv0  20324  wilthlem3  20845  chtub  20988  2sqlem10  21150  pntpbnd1  21272  usgrarnedg  21396  usgraedg4  21398  isch3  22736  shmodsi  22883  orthin  22940  h1datomi  23075  stcltr2i  23770  atom1d  23848  sumdmdii  23910  cdj3lem1  23929  disjpreima  24018  kerf1hrm  24254  lmxrge0  24329  dmvlsiga  24504  sibfof  24646  erdszelem9  24877  cvmlift2lem1  24981  fundmpss  25382  tfisg  25471  wfisg  25476  frinsg  25512  poseq  25520  sltval2  25603  nodenselem7  25634  nofulllem5  25653  mptelee  25826  axeuclidlem  25893  axcontlem4  25898  outsideofrflx  26053  mblfinlem2  26235  itg2addnclem3  26248  nn0prpwlem  26316  ivthALT  26329  fnessref  26364  neibastop2lem  26380  tailfb  26397  cover2  26406  fdc  26440  nninfnub  26446  equivtotbnd  26478  prdstotbnd  26494  cntotbnd  26496  ablo4pnp  26546  isdrngo3  26566  crngohomfo  26607  intidl  26630  prtlem90  26697  prtlem18  26717  prter2  26721  2reu1  27931  swrdnd  28154  swrdvalodmlem1  28159  swrdccatin2  28176  2cshw1lem2  28215  lswrdn0  28226  frgrancvvdeqlemA  28363  frgrancvvdeqlemC  28365  alrim3con13v  28554  tratrb  28557  onfrALTlem3  28567  onfrALTlem2  28569  onfrALTlem1  28571  trsspwALT2  28869  trsspwALT3  28870  bnj600  29227  bnj1018  29270  bnj1173  29308  bnj1174  29309  lsat0cv  29768  lfl1  29805  lkreqN  29905  atlrelat1  30056  pmaple  30495  pmapsub  30502  pclclN  30625  pclfinN  30634  osumcllem4N  30693  pexmidlem1N  30704  cdleme7ga  30982  lcfl7N  32236
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator