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  1358  nic-ax  1429  nfimd  1786  equs5e  1860  euim  2226  mopick2  2243  2moswap  2251  2eu1  2256  necon3ad  2515  necon3d  2517  necon1d  2548  ralrimd  2665  spcimegf  2896  spcegf  2898  spcimedv  2901  spc2gv  2905  spc3gv  2907  rspcimedv  2920  eqsbc3r  3082  ra5  3109  tpid3g  3775  pwpw0  3800  sssn  3809  pwsnALT  3859  ssiun  3981  ssiun2  3982  wefrc  4424  tron  4452  ordtri3or  4461  oneqmini  4480  reusv6OLD  4582  nnsuc  4710  dmcosseq  4983  relssres  5029  trin2  5103  ssrnres  5153  sossfld  5157  fnun  5387  f1oun  5530  brprcneu  5556  ssimaex  5622  chfnrn  5674  dffo4  5714  dffo5  5715  fvclss  5801  isomin  5876  isofrlem  5879  isoselem  5880  f1oweALT  5893  fnoprabg  5987  frxp  6267  poxp  6269  fnse  6274  issmo2  6408  smores  6411  smogt  6426  rdglim2  6487  tz7.48lem  6495  tz7.49  6499  swoer  6730  qsss  6762  domtriord  7050  pssnn  7124  ssfi  7126  findcard  7142  findcard2  7143  findcard3  7145  frfi  7147  dffi3  7229  supmo  7248  inf3lem4  7377  carddom2  7655  fidomtri2  7672  pm54.43  7678  infpwfien  7734  alephordi  7746  cardaleph  7761  carduniima  7768  cardinfima  7769  alephval3  7782  dfac5lem4  7798  dfac5  7800  dfac2  7802  kmlem2  7822  cflm  7921  cfslb2n  7939  cfsmolem  7941  isf32lem9  8032  axcc4  8110  domtriomlem  8113  zorn2lem4  8171  zorn2lem6  8173  fpwwe2lem11  8307  fpwwe2lem12  8308  inttsk  8441  inar1  8442  intgru  8481  ingru  8482  indpi  8576  nqpr  8683  ltaddpr  8703  ltexprlem1  8705  ltexprlem5  8709  reclem2pr  8717  reclem4pr  8719  zmulcl  10113  uzm1  10305  uzwo  10328  uzwoOLD  10329  negn0  10351  xmullem2  10632  icoshft  10805  difreicc  10814  fzouzsplit  10948  seqf1olem1  11132  seqf1olem2  11133  incexclem  12342  sqr2irr  12574  dvds2lem  12588  dvdslelem  12620  divalglem8  12646  euclemma  12834  iserodd  12935  ramcl  13123  mreiincl  13547  dirge  14408  sylow2alem1  14977  efgredlemb  15104  lbspss  15884  lspsneu  15925  lspsnat  15947  lspsncv0  15948  opsrtoslem2  16275  distop  16789  epttop  16802  isclo2  16881  restdis  16965  subbascn  17040  cnrest2  17070  cnpresti  17072  isnrm2  17142  cmpsublem  17182  cmpcld  17185  dfcon2  17201  t1conperf  17218  1stcrest  17235  lly1stc  17278  uptx  17375  txcn  17376  prdstopn  17378  txcon  17439  cmphaushmeo  17547  fbasrn  17631  csdfil  17641  trufil  17657  fclscf  17772  alexsubALTlem3  17795  alexsubALT  17797  haustsms2  17871  ovoliunlem1  18914  ovoliunnul  18919  volsup2  19013  coeaddlem  19683  plymul0or  19714  radcnv0  19845  wilthlem3  20361  chtub  20504  2sqlem10  20666  pntpbnd1  20788  isch3  21876  shmodsi  22023  orthin  22080  h1datomi  22215  stcltr2i  22910  atom1d  22988  sumdmdii  23050  cdj3lem1  23069  disjpreima  23169  kerf1hrm  23542  dmvlsiga  23688  erdszelem9  24014  cvmlift2lem1  24117  fundmpss  24507  tfisg  24589  wfisg  24594  frinsg  24630  poseq  24638  sltval2  24695  nodenselem7  24726  nofulllem5  24745  mptelee  24909  axeuclidlem  24976  axcontlem4  24981  outsideofrflx  25136  nn0prpwlem  25387  ivthALT  25407  fnessref  25442  neibastop2lem  25458  tailfb  25475  cover2  25507  fdc  25604  nninfnub  25610  equivtotbnd  25650  prdstotbnd  25666  cntotbnd  25668  ablo4pnp  25718  isdrngo3  25738  crngohomfo  25779  intidl  25802  prtlem90  25871  prtlem18  25893  prter2  25897  2reu1  27112  bropopvvv  27252  mpt2xopynvov0g  27254  hashtpg  27279  usgrarnedg  27355  usgraedg4  27357  frgrancvvdeqlemA  27629  frgrancvvdeqlemC  27631  alrim3con13v  27790  tratrb  27793  onfrALTlem3  27803  onfrALTlem2  27805  onfrALTlem1  27807  trsspwALT2  28104  trsspwALT3  28105  pwtrOLD  28110  bnj600  28462  bnj1018  28505  bnj1173  28543  bnj1174  28544  a12study3  28953  lsat0cv  29041  lfl1  29078  lkreqN  29178  atlrelat1  29329  pmaple  29768  pmapsub  29775  pclclN  29898  pclfinN  29907  osumcllem4N  29966  pexmidlem1N  29977  cdleme7ga  30255  lcfl7N  31509
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