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  1490  nfimd  1864  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  euim  2346  mopick2  2370  2moswap  2378  2eu1OLD  2387  2eu6  2393  necon3adOLD  2678  necon3d  2691  necon1d  2692  ralrimd  2868  spcimegf  3192  spcegf  3194  spcimedv  3197  spc2gv  3201  spc3gv  3203  rspcimedv  3216  eqsbc3r  3393  ra4  3427  tpid3g  4142  pwpw0  4175  sssn  4185  pwsnALT  4240  ssiun  4367  ssiun2  4368  reusv6OLD  4658  wefrc  4873  tron  4901  ordtri3or  4910  oneqmini  4929  dmcosseq  5262  relssres  5309  restidsing  5328  trin2  5388  ssrnres  5443  sossfld  5452  fnun  5685  f1oun  5833  brprcneu  5857  ssimaex  5930  chfnrn  5990  dffo4  6035  dffo5  6036  fvclss  6140  isomin  6219  isofrlem  6222  isoselem  6223  fnoprabg  6385  nnsuc  6695  f1oweALT  6765  bropopvvv  6860  frxp  6890  poxp  6892  fnse  6897  mpt2xopynvov0g  6939  issmo2  7017  smores  7020  smogt  7035  rdglim2  7095  tz7.48lem  7103  tz7.49  7107  swoer  7336  qsss  7369  domtriord  7660  pssnn  7735  ssfi  7737  findcard  7755  findcard2  7756  findcard3  7759  frfi  7761  dffi3  7887  supmo  7908  inf3lem4  8044  carddom2  8354  fidomtri2  8371  pm54.43  8377  infpwfien  8439  alephordi  8451  cardaleph  8466  carduniima  8473  cardinfima  8474  alephval3  8487  dfac5lem4  8503  dfac5  8505  dfac2  8507  kmlem2  8527  cflm  8626  cfslb2n  8644  cfsmolem  8646  isf32lem9  8737  axcc4  8815  domtriomlem  8818  zorn2lem4  8875  zorn2lem6  8877  fpwwe2lem11  9014  fpwwe2lem12  9015  inttsk  9148  inar1  9149  intgru  9188  ingru  9189  indpi  9281  nqpr  9388  ltaddpr  9408  ltexprlem1  9410  ltexprlem5  9414  reclem2pr  9422  reclem4pr  9424  zmulcl  10907  uzm1  11108  uzwo  11140  uzwoOLD  11141  negn0  11164  xmullem2  11453  icoshft  11638  difreicc  11648  fzouzsplit  11824  ssfzoulel  11870  seqf1olem1  12110  seqf1olem2  12111  hashtpg  12485  swrdnd  12616  swrdccatin2  12671  modfsummod  13567  incexclem  13607  sqrt2irr  13839  dvds2lem  13853  dvdslelem  13885  divalglem8  13913  euclemma  14104  iserodd  14214  ramcl  14402  mreiincl  14847  joinfval  15484  meetfval  15498  dirge  15720  sylow2alem1  16433  efgredlemb  16560  kerf1hrm  17175  lbspss  17511  lspsneu  17552  lspsnat  17574  lspsncv0  17575  opsrtoslem2  17920  distop  19263  epttop  19276  isclo2  19355  restdis  19445  subbascn  19521  cnrest2  19553  cnpresti  19555  isnrm2  19625  cmpsublem  19665  cmpcld  19668  dfcon2  19686  t1conperf  19703  1stcrest  19720  lly1stc  19763  uptx  19861  txcn  19862  prdstopn  19864  txcon  19925  cmphaushmeo  20036  fbasrn  20120  csdfil  20130  trufil  20146  fclscf  20261  alexsubALTlem3  20284  alexsubALT  20286  haustsms2  20370  ovoliunlem1  21648  ovoliunnul  21653  volsup2  21749  coeaddlem  22380  plymul0or  22411  radcnv0  22545  wilthlem3  23072  chtub  23215  2sqlem10  23377  pntpbnd1  23499  mptelee  23874  axeuclidlem  23941  axcontlem4  23946  usgrarnedg  24060  usgraedg4  24063  frgrancvvdeqlemA  24714  frgrancvvdeqlemC  24716  isch3  25835  shmodsi  25983  orthin  26040  h1datomi  26175  stcltr2i  26870  atom1d  26948  sumdmdii  27010  cdj3lem1  27029  disjpreima  27118  suppss3  27222  lmxrge0  27570  dmvlsiga  27769  sibfof  27922  erdszelem9  28283  cvmlift2lem1  28387  fundmpss  28773  tfisg  28861  wfisg  28866  frinsg  28902  poseq  28910  sltval2  28993  nodenselem7  29024  nofulllem5  29043  outsideofrflx  29354  mblfinlem3  29630  itg2addnclem3  29645  nn0prpwlem  29717  ivthALT  29730  fnessref  29765  neibastop2lem  29781  tailfb  29798  cover2  29807  fdc  29841  nninfnub  29847  equivtotbnd  29877  prdstotbnd  29893  cntotbnd  29895  ablo4pnp  29945  isdrngo3  29965  crngohomfo  30006  intidl  30029  or32dd  30097  prtlem90  30202  prtlem18  30222  prter2  30226  nzss  30822  2reu1  31658  lswn0  31812  usgedgimp  31872  usgedgimpALT  31875  3impexpbicom  32300  alrim3con13v  32383  tratrb  32386  onfrALTlem3  32396  onfrALTlem2  32398  onfrALTlem1  32400  trsspwALT2  32697  trsspwALT3  32698  bnj600  33056  bnj1018  33099  bnj1173  33137  bnj1174  33138  bj-axtd  33264  bj-nfdt0  33330  bj-2upleq  33651  lsat0cv  33830  lfl1  33867  lkreqN  33967  atlrelat1  34118  pmaple  34557  pmapsub  34564  pclclN  34687  pclfinN  34696  osumcllem4N  34755  pexmidlem1N  34766  cdleme7ga  35044  lcfl7N  36298
  Copyright terms: Public domain W3C validator