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

Theorem syl5ibr 214
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 194 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 212 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  syl5ibrcom  215  biimprd  216  dvelimvOLD  2032  exdistrf  2070  pm2.61ne  2686  unineq  3579  oteqex  4484  ordtri3  4652  limelon  4679  eldifpw  4790  ssonuni  4802  onsucuni2  4849  ordzsl  4860  tfindsg  4875  findsg  4907  elrnmpt1  5154  cnveqb  5361  cnveq0  5362  relcoi1  5433  ndmfv  5786  ffvresb  5936  isomin  6093  isofrlem  6096  caovord3d  6293  frxp  6492  poxp  6494  fnwelem  6497  tfrlem1  6672  tfrlem11  6685  oacl  6815  omcl  6816  oecl  6817  oa0r  6818  om0r  6819  om1r  6822  oe1m  6824  oaordi  6825  oawordri  6829  oaass  6840  oarec  6841  omwordri  6851  odi  6858  omass  6859  oewordri  6871  oeworde  6872  oeordsuc  6873  oelim2  6874  oeoa  6876  oeoelem  6877  oeoe  6878  nnm0r  6889  nnacl  6890  nnacom  6896  nnaordi  6897  nnaass  6901  nndi  6902  nnmass  6903  nnmsucr  6904  nnmcom  6905  omabs  6926  brecop  7033  eceqoveq  7045  elpm2r  7070  map0g  7089  undifixp  7134  fundmen  7216  mapxpen  7309  mapunen  7312  php  7327  unxpdomlem2  7350  pssnn  7363  elfir  7456  wemapso2  7557  wdompwdom  7582  inf3lem1  7619  inf3lem3  7621  noinfepOLD  7651  cantnfval2  7660  cantnfp1lem3  7672  r1sdom  7736  r1tr  7738  carden2a  7891  fidomtri2  7919  prdom2  7928  infxpenlem  7933  acndom  7970  fodomacn  7975  wdomfil  7980  alephon  7988  alephordi  7993  alephle  8007  alephfplem3  8025  dfac2a  8048  kmlem9  8076  cflm  8168  cfslb  8184  cfslbn  8185  infpssrlem3  8223  infpssrlem4  8224  fin23lem21  8257  fin23lem30  8260  isf34lem7  8297  isf34lem6  8298  fin67  8313  isfin7-2  8314  fin1a2lem7  8324  fin1a2lem10  8327  iundom2g  8453  konigthlem  8481  alephreg  8495  gchdomtri  8542  wunr1om  8632  tskr1om  8680  inar1  8688  grur1a  8732  indpi  8822  genpprecl  8916  genpnmax  8922  addcmpblnr  8985  recexsrlem  9016  map2psrpr  9023  ax1rid  9074  axpre-mulgt0  9081  ltle  9201  nnmulcl  10061  nnsub  10076  nn0sub  10308  nneo  10391  uzindOLD  10402  uz11  10546  xrltle  10780  xltnegi  10840  xrsupsslem  10923  xrinfmsslem  10924  xrub  10928  supxrunb1  10936  supxrunb2  10937  om2uzuzi  11327  uzrdgxfr  11344  seqcl2  11379  seqfveq2  11383  seqshft2  11387  seqsplit  11394  seqcaopr3  11396  seqf1olem2a  11399  seqid2  11407  seqhomo  11408  ser1const  11417  m1expcl2  11441  expadd  11460  expmul  11463  faclbnd  11619  hashmap  11736  hashfacen  11741  hashf1lem1  11742  hashf1lem2  11743  hashf1  11744  seqcoll  11750  recan  12178  rexanre  12188  rlimcn2  12422  caurcvg2  12509  fsumiun  12638  efexp  12740  rpnnen2  12863  dvdstr  12921  alzdvds  12937  bitsinv1  12992  smu01lem  13035  smupval  13038  smueqlem  13040  smumullem  13042  seq1st  13100  prmdiveq  13213  odzdvds  13219  pythagtriplem2  13229  pcexp  13271  vdwlem13  13399  ramz  13431  elrestr  13694  xpsff1o  13831  subsubc  14088  frmdgsum  14845  mulgneg2  14955  mulgnnass  14956  mhmmulg  14960  symgbas  15133  gsumwrev  15200  sylow1lem1  15270  efgsfo  15409  efgred  15418  cyggexb  15546  gsum2d  15584  mulgass2  15748  lmodprop2d  16044  lspsnne2  16228  lspsneu  16233  assapropd  16424  mplcoe1  16566  mplcoe3  16567  mplcoe2  16568  ply1sclf1  16718  cnfldmulg  16771  cnfldexp  16772  restopn2  17279  cnpf2  17352  cmpfi  17509  txcn  17696  txlm  17718  xkoptsub  17724  xkopjcn  17726  ufildr  18001  cnflf  18072  fclsnei  18089  fclscmp  18100  ufilcmp  18102  cnfcf  18112  symgtgp  18169  isxms2  18516  met2ndc  18591  metustblOLD  18648  metustbl  18649  tngngp2  18731  clmmulg  19156  iscau4  19270  ovolunlem1a  19430  ovolicc2lem4  19454  volfiniun  19479  voliunlem1  19482  volsup  19488  dvnadd  19853  dvnres  19855  dvcobr  19870  ply1nzb  20083  plypf1  20169  dgrle  20200  coeaddlem  20205  dgrlt  20222  dvntaylp  20325  cxpmul2  20618  rlimcnp  20842  wilthlem2  20890  isnsqf  20956  musum  21014  chtub  21034  chpval2  21040  dchrisumlem1  21221  qabvexp  21358  ostthlem2  21360  usgra2edg  21440  cusgrafilem1  21526  sizeusglecusglem1  21531  sizeusglecusg  21533  trliswlk  21577  2trllemF  21587  constr3lem6  21674  1conngra  21700  hashnbgravdg  21720  eupatrl  21728  isexid2  21951  ismndo1  21970  rngo2  22014  rngoueqz  22056  sspval  22260  nmosetre  22303  nmobndseqi  22318  nmobndseqiOLD  22319  orthcom  22648  shsva  22860  shmodsi  22929  h1datomi  23121  nmopsetretALT  23404  nmfnsetre  23418  lnopcnbd  23577  pjclem4  23740  pj3si  23748  ssmd1  23852  atom1d  23894  chjatom  23898  atcvat4i  23938  cdj3lem2a  23977  cdj3lem3a  23980  unitdivcld  24334  xrge0iifiso  24356  dya2iocuni  24668  facgam  24885  deranglem  24887  subfacp1lem6  24906  subfacval2  24908  cvmlift2lem12  25036  relexpsucr  25165  relexpsucl  25167  relexprel  25169  relexpdm  25170  relexprn  25171  relexpadd  25173  relexpindlem  25174  relexpind  25175  rtrclreclem.trans  25181  rtrclreclem.min  25182  dfrtrcl2  25183  rtrclind  25184  dfon2lem6  25450  rdgprc  25457  predpoirr  25507  predfrirr  25508  trpredlem1  25540  wfrlem14  25586  frrlem5e  25625  nodenselem8  25678  axsegconlem1  25891  ax5seglem4  25906  ax5seglem5  25907  axlowdimlem15  25930  axcontlem2  25939  axcontlem4  25941  ifscgr  26013  btwncolinear1  26038  hfelhf  26157  ordcmp  26232  findreccl  26238  nndivlub  26243  opnrebl2  26366  nn0prpw  26368  eqfnun  26465  sdclem2  26488  sdclem1  26489  prdsbnd2  26546  ismtyval  26551  rrnequiv  26586  exidreslem  26594  risci  26645  prtlem11  26827  prtlem15  26836  aovmpt4g  28153  otel3xp  28175  oteqimp  28176  wrdsymb0  28300  swrdvalodm2  28320  swrdvalodm  28321  swrdccatin12lem3  28344  swrdccatin2d  28353  2cshwmod  28389  lswrd0  28393  wlkiswwlk2lem4  28474  el2wlkonot  28499  el2spthonot  28500  frgra3vlem1  28562  3vfriswmgralem  28566  frconngra  28583  frgrawopreglem3  28607  frg2wot1  28618  2spotiundisj  28623  usg2spot2nb  28626  usgreg2spot  28628  bnj168  29271  bnj535  29435  bnj590  29455  bnj594  29457  bnj938  29482  bnj1118  29527  bnj1128  29533  dvelimvNEW7  29636  cvrat4  30414  lcfl6  32472
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