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

Theorem syl6ibr 218
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 197 . 2  |-  ( ch 
->  th )
41, 3syl6 29 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr4g  261  imp4a  572  3impexpbicom  1357  nic-ax  1428  equs5e  1829  euim  2193  mopick2  2210  2moswap  2218  2eu1  2223  necon3ad  2482  necon3d  2484  necon1d  2515  ralrimd  2631  spcimegf  2862  spcegf  2864  spcimedv  2867  spc2gv  2871  spc3gv  2873  rspcimedv  2886  eqsbc3r  3048  ra5  3075  tpid3g  3741  pwpw0  3763  sssn  3772  pwsnALT  3822  ssiun  3944  ssiun2  3945  wefrc  4387  tron  4415  ordtri3or  4424  oneqmini  4443  reusv6OLD  4545  nnsuc  4673  dmcosseq  4946  relssres  4992  trin2  5066  ssrnres  5116  sossfld  5120  fnun  5350  f1oun  5492  brprcneu  5518  ssimaex  5584  chfnrn  5636  dffo4  5676  dffo5  5677  fvclss  5760  isomin  5834  isofrlem  5837  isoselem  5838  f1oweALT  5851  fnoprabg  5945  frxp  6225  poxp  6227  fnse  6232  issmo2  6366  smores  6369  smogt  6384  rdglim2  6445  tz7.48lem  6453  tz7.49  6457  swoer  6688  qsss  6720  domtriord  7007  pssnn  7081  ssfi  7083  findcard  7097  findcard2  7098  findcard3  7100  frfi  7102  dffi3  7184  supmo  7203  inf3lem4  7332  carddom2  7610  fidomtri2  7627  pm54.43  7633  infpwfien  7689  alephordi  7701  cardaleph  7716  carduniima  7723  cardinfima  7724  alephval3  7737  dfac5lem4  7753  dfac5  7755  dfac2  7757  kmlem2  7777  cflm  7876  cfslb2n  7894  cfsmolem  7896  isf32lem9  7987  axcc4  8065  domtriomlem  8068  zorn2lem4  8126  zorn2lem6  8128  fpwwe2lem11  8262  fpwwe2lem12  8263  inttsk  8396  inar1  8397  intgru  8436  ingru  8437  indpi  8531  nqpr  8638  ltaddpr  8658  ltexprlem1  8660  ltexprlem5  8664  reclem2pr  8672  reclem4pr  8674  zmulcl  10066  uzm1  10258  uzwo  10281  uzwoOLD  10282  negn0  10304  xmullem2  10585  icoshft  10758  difreicc  10767  fzouzsplit  10901  seqf1olem1  11085  seqf1olem2  11086  incexclem  12295  sqr2irr  12527  dvds2lem  12541  dvdslelem  12573  divalglem8  12599  euclemma  12787  iserodd  12888  ramcl  13076  mreiincl  13498  dirge  14359  sylow2alem1  14928  efgredlemb  15055  lbspss  15835  lspsneu  15876  lspsnat  15898  lspsncv0  15899  opsrtoslem2  16226  distop  16733  epttop  16746  isclo2  16825  restdis  16909  subbascn  16984  cnrest2  17014  cnpresti  17016  isnrm2  17086  cmpsublem  17126  cmpcld  17129  dfcon2  17145  t1conperf  17162  1stcrest  17179  lly1stc  17222  uptx  17319  txcn  17320  prdstopn  17322  txcon  17383  cmphaushmeo  17491  fbasrn  17579  csdfil  17589  trufil  17605  fclscf  17720  alexsubALTlem3  17743  alexsubALT  17745  haustsms2  17819  ovoliunlem1  18861  ovoliunnul  18866  volsup2  18960  coeaddlem  19630  plymul0or  19661  radcnv0  19792  wilthlem3  20308  chtub  20451  2sqlem10  20613  pntpbnd1  20735  isch3  21821  shmodsi  21968  orthin  22025  h1datomi  22160  stcltr2i  22855  atom1d  22933  sumdmdii  22995  cdj3lem1  23014  disjpreima  23361  dmvlsiga  23490  erdszelem9  23730  cvmlift2lem1  23833  fundmpss  24122  tfisg  24204  wfisg  24209  frinsg  24245  poseq  24253  sltval2  24310  nodenselem7  24341  nofulllem5  24360  mptelee  24523  axeuclidlem  24590  axcontlem4  24595  outsideofrflx  24750  untim1d  25020  untim2d  25021  restidsing  25076  defse3  25272  inttop2  25515  rdmob  25748  dualcat2  25784  nn0prpwlem  26238  ivthALT  26258  fnessref  26293  neibastop2lem  26309  tailfb  26326  cover2  26358  fdc  26455  nninfnub  26461  equivtotbnd  26502  prdstotbnd  26518  cntotbnd  26520  ablo4pnp  26570  isdrngo3  26590  crngohomfo  26631  intidl  26654  prtlem90  26723  prtlem18  26745  prter2  26749  2reu1  27964  mpt2xopynvov0g  28080  alrim3con13v  28296  tratrb  28299  onfrALTlem3  28309  onfrALTlem2  28311  onfrALTlem1  28313  trsspwALT2  28593  trsspwALT3  28594  pwtrOLD  28599  bnj600  28951  bnj1018  28994  bnj1173  29032  bnj1174  29033  a12study3  29135  lsat0cv  29223  lfl1  29260  lkreqN  29360  atlrelat1  29511  pmaple  29950  pmapsub  29957  pclclN  30080  pclfinN  30089  osumcllem4N  30148  pexmidlem1N  30159  cdleme7ga  30437  lcfl7N  31691
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 177
  Copyright terms: Public domain W3C validator