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

Theorem syl6ibr 220
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 199 . 2  |-  ( ch 
->  th )
41, 3syl6 32 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  3imtr4g  263  imp4a  574  3impexpbicom  1377  nic-ax  1448  nfimd  1828  equs5eOLD  1912  ax12olem2  2007  ax12olem2OLD  2013  euim  2333  mopick2  2350  2moswap  2358  2eu1  2363  necon3ad  2639  necon3d  2641  necon1d  2675  ralrimd  2796  spcimegf  3032  spcegf  3034  spcimedv  3037  spc2gv  3041  spc3gv  3043  rspcimedv  3056  eqsbc3r  3220  ra5  3247  tpid3g  3921  pwpw0  3948  sssn  3959  pwsnALT  4012  ssiun  4135  ssiun2  4136  wefrc  4579  tron  4607  ordtri3or  4616  oneqmini  4635  reusv6OLD  4737  nnsuc  4865  dmcosseq  5140  relssres  5186  trin2  5260  ssrnres  5312  sossfld  5320  fnun  5554  f1oun  5697  brprcneu  5724  ssimaex  5791  chfnrn  5844  dffo4  5888  dffo5  5889  fvclss  5983  isomin  6060  isofrlem  6063  isoselem  6064  f1oweALT  6077  fnoprabg  6174  bropopvvv  6429  frxp  6459  poxp  6461  fnse  6466  mpt2xopynvov0g  6468  issmo2  6614  smores  6617  smogt  6632  rdglim2  6693  tz7.48lem  6701  tz7.49  6705  swoer  6936  qsss  6968  domtriord  7256  pssnn  7330  ssfi  7332  findcard  7350  findcard2  7351  findcard3  7353  frfi  7355  dffi3  7439  supmo  7460  inf3lem4  7589  carddom2  7869  fidomtri2  7886  pm54.43  7892  infpwfien  7948  alephordi  7960  cardaleph  7975  carduniima  7982  cardinfima  7983  alephval3  7996  dfac5lem4  8012  dfac5  8014  dfac2  8016  kmlem2  8036  cflm  8135  cfslb2n  8153  cfsmolem  8155  isf32lem9  8246  axcc4  8324  domtriomlem  8327  zorn2lem4  8384  zorn2lem6  8386  fpwwe2lem11  8520  fpwwe2lem12  8521  inttsk  8654  inar1  8655  intgru  8694  ingru  8695  indpi  8789  nqpr  8896  ltaddpr  8916  ltexprlem1  8918  ltexprlem5  8922  reclem2pr  8930  reclem4pr  8932  zmulcl  10329  uzm1  10521  uzwo  10544  uzwoOLD  10545  negn0  10567  xmullem2  10849  icoshft  11024  difreicc  11033  fzouzsplit  11173  seqf1olem1  11367  seqf1olem2  11368  hashtpg  11696  incexclem  12621  sqr2irr  12853  dvds2lem  12867  dvdslelem  12899  divalglem8  12925  euclemma  13113  iserodd  13214  ramcl  13402  mreiincl  13826  dirge  14687  sylow2alem1  15256  efgredlemb  15383  lbspss  16159  lspsneu  16200  lspsnat  16222  lspsncv0  16223  opsrtoslem2  16550  distop  17065  epttop  17078  isclo2  17157  restdis  17247  subbascn  17323  cnrest2  17355  cnpresti  17357  isnrm2  17427  cmpsublem  17467  cmpcld  17470  dfcon2  17487  t1conperf  17504  1stcrest  17521  lly1stc  17564  uptx  17662  txcn  17663  prdstopn  17665  txcon  17726  cmphaushmeo  17837  fbasrn  17921  csdfil  17931  trufil  17947  fclscf  18062  alexsubALTlem3  18085  alexsubALT  18087  haustsms2  18171  ovoliunlem1  19403  ovoliunnul  19408  volsup2  19502  coeaddlem  20172  plymul0or  20203  radcnv0  20337  wilthlem3  20858  chtub  21001  2sqlem10  21163  pntpbnd1  21285  usgrarnedg  21409  usgraedg4  21411  isch3  22749  shmodsi  22896  orthin  22953  h1datomi  23088  stcltr2i  23783  atom1d  23861  sumdmdii  23923  cdj3lem1  23942  disjpreima  24031  kerf1hrm  24267  lmxrge0  24342  dmvlsiga  24517  sibfof  24659  erdszelem9  24890  cvmlift2lem1  24994  fundmpss  25395  tfisg  25484  wfisg  25489  frinsg  25525  poseq  25533  sltval2  25616  nodenselem7  25647  nofulllem5  25666  mptelee  25839  axeuclidlem  25906  axcontlem4  25911  outsideofrflx  26066  mblfinlem3  26257  itg2addnclem3  26272  nn0prpwlem  26339  ivthALT  26352  fnessref  26387  neibastop2lem  26403  tailfb  26420  cover2  26429  fdc  26463  nninfnub  26469  equivtotbnd  26501  prdstotbnd  26517  cntotbnd  26519  ablo4pnp  26569  isdrngo3  26589  crngohomfo  26630  intidl  26653  prtlem90  26720  prtlem18  26740  prter2  26744  2reu1  27954  swrdnd  28216  swrdvalodmlem1  28221  swrdccatin2  28244  2cshw1lem2  28283  lswrdn0  28294  frgrancvvdeqlemA  28500  frgrancvvdeqlemC  28502  alrim3con13v  28691  tratrb  28694  onfrALTlem3  28704  onfrALTlem2  28706  onfrALTlem1  28708  trsspwALT2  29006  trsspwALT3  29007  bnj600  29364  bnj1018  29407  bnj1173  29445  bnj1174  29446  lsat0cv  29905  lfl1  29942  lkreqN  30042  atlrelat1  30193  pmaple  30632  pmapsub  30639  pclclN  30762  pclfinN  30771  osumcllem4N  30830  pexmidlem1N  30841  cdleme7ga  31119  lcfl7N  32373
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 179
  Copyright terms: Public domain W3C validator