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

Theorem syl5ibr 221
Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)
Hypotheses
Ref Expression
syl5ibr.1  |-  ( ph  ->  th )
syl5ibr.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ibr  |-  ( ch 
->  ( ph  ->  ps ) )

Proof of Theorem syl5ibr
StepHypRef Expression
1 syl5ibr.1 . 2  |-  ( ph  ->  th )
2 syl5ibr.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
32bicomd 201 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 219 1  |-  ( ch 
->  ( ph  ->  ps ) )
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:  syl5ibrcom  222  biimprd  223  exdistrf  2024  pm2.61ne  2676  unineq  3588  oteqex  4572  ordtri3  4742  limelon  4769  elrnmpt1  5075  cnveqb  5281  cnveq0  5282  relcoi1  5354  ndmfv  5702  ffvresb  5861  isomin  6015  isofrlem  6018  caovord3d  6262  eldifpw  6377  ssonuni  6387  onsucuni2  6434  ordzsl  6445  tfindsg  6460  findsg  6492  frxp  6671  poxp  6673  fnwelem  6676  suppss  6708  tfrlem11  6833  oacl  6963  omcl  6964  oecl  6965  oa0r  6966  om0r  6967  om1r  6970  oe1m  6972  oaordi  6973  oawordri  6977  oaass  6988  oarec  6989  omwordri  6999  odi  7006  omass  7007  oewordri  7019  oeworde  7020  oeordsuc  7021  oelim2  7022  oeoa  7024  oeoelem  7025  oeoe  7026  nnm0r  7037  nnacl  7038  nnacom  7044  nnaordi  7045  nnaass  7049  nndi  7050  nnmass  7051  nnmsucr  7052  nnmcom  7053  omabs  7074  brecop  7181  eceqoveq  7193  elpm2r  7218  map0g  7240  undifixp  7287  fundmen  7371  mapxpen  7465  mapunen  7468  php  7483  unxpdomlem2  7506  pssnn  7519  elfir  7653  wemapso2OLD  7754  wemapso2lem  7755  wdompwdom  7781  inf3lem1  7822  inf3lem3  7824  noinfepOLD  7854  cantnfval2  7865  cantnfp1lem3  7876  cantnfval2OLD  7895  cantnfp1lem3OLD  7902  r1sdom  7969  r1tr  7971  carden2a  8124  fidomtri2  8152  prdom2  8161  infxpenlem  8168  acndom  8209  fodomacn  8214  wdomfil  8219  alephon  8227  alephordi  8232  alephle  8246  alephfplem3  8264  dfac2a  8287  kmlem9  8315  cflm  8407  cfslb  8423  cfslbn  8424  infpssrlem3  8462  infpssrlem4  8463  fin23lem21  8496  fin23lem30  8499  isf34lem7  8536  isf34lem6  8537  fin67  8552  isfin7-2  8553  fin1a2lem7  8563  fin1a2lem10  8566  iundom2g  8692  konigthlem  8720  alephreg  8734  gchdomtri  8783  wunr1om  8873  tskr1om  8921  inar1  8929  grur1a  8973  indpi  9063  genpprecl  9157  genpnmax  9163  addcmpblnr  9226  recexsrlem  9257  map2psrpr  9264  ax1rid  9315  axpre-mulgt0  9322  ltle  9450  nnmulcl  10332  nnsub  10347  nn0sub  10617  nneo  10712  uzindOLD  10723  uz11  10870  xrltle  11113  xltnegi  11173  xrsupsslem  11256  xrinfmsslem  11257  xrub  11261  supxrunb1  11269  supxrunb2  11270  om2uzuzi  11755  uzrdgxfr  11772  seqcl2  11807  seqfveq2  11811  seqshft2  11815  seqsplit  11822  seqcaopr3  11824  seqf1olem2a  11827  seqid2  11835  seqhomo  11836  ser1const  11845  m1expcl2  11870  expadd  11889  expmul  11892  faclbnd  12049  hashmap  12180  hashfacen  12190  hashf1lem1  12191  hashf1lem2  12192  hashf1  12193  seqcoll  12199  wrdsymb0  12242  lsw0  12250  swrdvalodm2  12316  swrdvalodm  12317  wrd2ind  12355  swrdccatin12lem2  12363  swrdccatin1d  12373  repswccat  12406  repswcshw  12429  recan  12807  rexanre  12817  rlimcn2  13051  caurcvg2  13138  fsumiun  13266  efexp  13367  rpnnen2  13490  dvdstr  13548  alzdvds  13565  bitsinv1  13620  smu01lem  13663  smupval  13666  smueqlem  13668  smumullem  13670  seq1st  13728  prmdiveq  13843  odzdvds  13849  pythagtriplem2  13866  pcexp  13908  vdwlem13  14036  ramz  14068  elrestr  14349  xpsff1o  14488  subsubc  14745  clatl  15268  frmdgsum  15519  mulgneg2  15633  mulgnnass  15634  mhmmulg  15638  gsumwrev  15860  symgbas  15864  symgextf1lem  15904  symgfixelsi  15919  pmtrdifellem4  15964  sylow1lem1  16076  efgsfo  16215  efgred  16224  cyggexb  16354  gsumzres  16367  gsum2dlem2  16435  gsum2dOLD  16437  mulgass2  16626  lmodprop2d  16930  lspsnne2  17120  lspsneu  17125  assapropd  17319  mplcoe1  17477  mplcoe3  17478  mplcoe3OLD  17479  mplcoe2  17480  mplcoe2OLD  17481  ply1sclf1  17638  cnfldmulg  17691  cnfldexp  17692  zrhpsgnelbas  17865  restopn2  18622  cnpf2  18695  cmpfi  18852  txcn  19040  txlm  19062  xkoptsub  19068  xkopjcn  19070  ufildr  19345  cnflf  19416  fclsnei  19433  fclscmp  19444  ufilcmp  19446  cnfcf  19456  symgtgp  19513  isxms2  19864  met2ndc  19939  metustblOLD  19996  metustbl  19997  tngngp2  20079  clmmulg  20506  iscau4  20631  ovolunlem1a  20820  ovolicc2lem4  20844  volfiniun  20869  voliunlem1  20872  volsup  20878  dvnadd  21244  dvnres  21246  dvcobr  21261  ply1nzb  21478  plypf1  21564  dgrle  21595  coeaddlem  21600  dgrlt  21617  dvntaylp  21720  cxpmul2  22018  rlimcnp  22243  wilthlem2  22291  isnsqf  22357  musum  22415  chtub  22435  chpval2  22441  dchrisumlem1  22622  qabvexp  22759  ostthlem2  22761  axsegconlem1  22985  ax5seglem4  23000  ax5seglem5  23001  axlowdimlem15  23024  axcontlem2  23033  axcontlem4  23035  usgra2edg  23123  cusgrafilem1  23209  sizeusglecusglem1  23214  sizeusglecusg  23216  trliswlk  23260  2trllemF  23270  constr3lem6  23357  1conngra  23383  hashnbgravdg  23403  eupatrl  23411  isexid2  23634  ismndo1  23653  rngo2  23697  rngoueqz  23739  sspval  23943  nmosetre  23986  nmobndseqi  24001  nmobndseqiOLD  24002  orthcom  24332  shsva  24545  shmodsi  24614  h1datomi  24806  nmopsetretALT  25089  nmfnsetre  25103  lnopcnbd  25262  pjclem4  25425  pj3si  25433  ssmd1  25537  atom1d  25579  chjatom  25583  atcvat4i  25623  cdj3lem2a  25662  cdj3lem3a  25665  disjunsn  25759  unitdivcld  26184  xrge0iifiso  26218  dya2iocuni  26551  facgam  26899  deranglem  26901  subfacp1lem6  26920  subfacval2  26922  cvmlift2lem12  27050  relexpsucr  27178  relexpsucl  27180  relexprel  27182  relexpdm  27183  relexprn  27184  relexpadd  27186  relexpindlem  27187  relexpind  27188  rtrclreclem.trans  27194  rtrclreclem.min  27195  dfrtrcl2  27196  rtrclind  27197  dfon2lem6  27447  rdgprc  27454  predpoirr  27504  predfrirr  27505  trpredlem1  27537  wfrlem14  27583  frrlem5e  27622  nodenselem8  27675  ifscgr  27921  btwncolinear1  27946  hfelhf  28065  ordcmp  28140  findreccl  28146  nndivlub  28151  opnrebl2  28357  nn0prpw  28359  eqfnun  28456  sdclem2  28479  sdclem1  28480  prdsbnd2  28535  ismtyval  28540  rrnequiv  28575  exidreslem  28583  risci  28634  prtlem11  28853  prtlem15  28862  aovmpt4g  29950  otel3xp  29971  oteqimp  29972  wlkiswwlk2lem4  30171  wwlknredwwlkn0  30202  wwlkextwrd  30203  el2wlkonot  30231  el2spthonot  30232  clwlkisclwwlklem2a  30290  clwwlkf1  30301  erclwwlksym0  30321  erclwwlksym  30327  eleclclwwlknlem2  30334  erclwwlknsym  30343  wwlkextproplem1  30403  wwlkextprop  30406  frgra3vlem1  30435  3vfriswmgralem  30439  frconngra  30456  frgrawopreglem3  30482  frg2wot1  30493  2spotiundisj  30498  usg2spot2nb  30501  usgreg2spot  30503  extwwlkfablem2  30514  numclwwlkovf2ex  30522  extwwlkfab  30526  ellcoellss  30675  bnj168  31420  bnj535  31582  bnj590  31602  bnj594  31604  bnj938  31629  bnj1118  31674  bnj1128  31680  cvrat4  32657  lcfl6  34715
  Copyright terms: Public domain W3C validator