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

Theorem syl5ibr 212
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 192 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 210 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  syl5ibrcom  213  biimprd  214  dvelimv  1881  pm2.61ne  2522  unineq  3420  oteqex  4258  ordtri3  4427  limelon  4454  eldifpw  4565  ssonuni  4577  onsucuni2  4624  ordzsl  4635  tfindsg  4650  findsg  4682  elrnmpt1  4927  cnveqb  5128  relcoi1  5199  ndmfv  5514  ffvresb  5652  isomin  5796  isofrlem  5799  caovord3d  5992  frxp  6187  poxp  6189  fnwelem  6192  tfrlem1  6387  tfrlem11  6400  oacl  6530  omcl  6531  oecl  6532  oa0r  6533  om0r  6534  om1r  6537  oe1m  6539  oaordi  6540  oawordri  6544  oaass  6555  oarec  6556  omwordri  6566  odi  6573  omass  6574  oewordri  6586  oeworde  6587  oeordsuc  6588  oelim2  6589  oeoa  6591  oeoelem  6592  oeoe  6593  nnm0r  6604  nnacl  6605  nnacom  6611  nnaordi  6612  nnaass  6616  nndi  6617  nnmass  6618  nnmsucr  6619  nnmcom  6620  omabs  6641  brecop  6747  eceqoveq  6759  elpm2r  6784  map0g  6803  undifixp  6848  fundmen  6930  mapxpen  7023  mapunen  7026  php  7041  unxpdomlem2  7064  pssnn  7077  elfir  7165  wemapso2  7263  wdompwdom  7288  inf3lem1  7325  inf3lem3  7327  noinfepOLD  7357  cantnfval2  7366  cantnfp1lem3  7378  r1sdom  7442  r1tr  7444  carden2a  7595  fidomtri2  7623  prdom2  7632  infxpenlem  7637  acndom  7674  fodomacn  7679  wdomfil  7684  alephon  7692  alephordi  7697  alephle  7711  alephfplem3  7729  dfac2a  7752  kmlem9  7780  cflm  7872  cfslb  7888  cfslbn  7889  infpssrlem3  7927  infpssrlem4  7928  fin23lem21  7961  fin23lem30  7964  isf34lem7  8001  isf34lem6  8002  fin67  8017  isfin7-2  8018  fin1a2lem7  8028  fin1a2lem10  8031  iundom2g  8158  konigthlem  8186  alephreg  8200  gchdomtri  8247  wunr1om  8337  tskr1om  8385  inar1  8393  grur1a  8437  indpi  8527  genpprecl  8621  genpnmax  8627  addcmpblnr  8690  recexsrlem  8721  map2psrpr  8728  ax1rid  8779  axpre-mulgt0  8786  ltle  8906  nnmulcl  9765  nnsub  9780  nn0sub  10010  nneo  10091  uzindOLD  10102  uz11  10246  xrltle  10479  xltnegi  10539  xrsupsslem  10621  xrinfmsslem  10622  xrub  10626  supxrunb1  10634  supxrunb2  10635  om2uzuzi  11008  uzrdgxfr  11025  seqcl2  11060  seqfveq2  11064  seqshft2  11068  seqsplit  11075  seqcaopr3  11077  seqf1olem2a  11080  seqid2  11088  seqhomo  11089  ser1const  11098  m1expcl2  11121  expadd  11140  expmul  11143  faclbnd  11299  hashmap  11383  hashfacen  11388  hashf1lem1  11389  hashf1lem2  11390  hashf1  11391  seqcoll  11397  recan  11816  rexanre  11826  rlimcn2  12060  caurcvg2  12146  fsumiun  12275  efexp  12377  rpnnen2  12500  dvdstr  12558  alzdvds  12574  bitsinv1  12629  smu01lem  12672  smupval  12675  smueqlem  12677  smumullem  12679  seq1st  12737  prmdiveq  12850  odzdvds  12856  pythagtriplem2  12866  pcexp  12908  vdwlem13  13036  ramz  13068  elrestr  13329  xpsff1o  13466  subsubc  13723  frmdgsum  14480  mulgneg2  14590  mulgnnass  14591  mhmmulg  14595  symgbas  14768  gsumwrev  14835  sylow1lem1  14905  efgsfo  15044  efgred  15053  cyggexb  15181  gsum2d  15219  mulgass2  15383  lmodprop2d  15683  lspsnne2  15867  lspsneu  15872  assapropd  16063  mplcoe1  16205  mplcoe3  16206  mplcoe2  16207  ply1sclf1  16360  cnfldmulg  16402  cnfldexp  16403  restopn2  16904  cnpf2  16976  cmpfi  17131  txcn  17316  txlm  17338  xkoptsub  17344  xkopjcn  17346  ufildr  17622  cnflf  17693  fclsnei  17710  fclscmp  17721  ufilcmp  17723  cnfcf  17733  symgtgp  17780  isxms2  17990  met2ndc  18065  tngngp2  18164  clmmulg  18587  iscau4  18701  ovolunlem1a  18851  ovolicc2lem4  18875  volfiniun  18900  voliunlem1  18903  volsup  18909  dvnadd  19274  dvnres  19276  dvcobr  19291  ply1nzb  19504  plypf1  19590  dgrle  19621  coeaddlem  19626  dgrlt  19643  dvntaylp  19746  cxpmul2  20032  rlimcnp  20256  wilthlem2  20303  isnsqf  20369  musum  20427  chtub  20447  chpval2  20453  dchrisumlem1  20634  qabvexp  20771  ostthlem2  20773  isexid2  20986  ismndo1  21005  rngo2  21049  rngoueqz  21091  sspval  21293  nmosetre  21336  nmobndseqi  21351  nmobndseqiOLD  21352  orthcom  21683  shsva  21895  shmodsi  21964  h1datomi  22156  nmopsetretALT  22439  nmfnsetre  22453  lnopcnbd  22612  pjclem4  22775  pj3si  22783  ssmd1  22887  atom1d  22929  chjatom  22933  atcvat4i  22973  cdj3lem2a  23012  cdj3lem3a  23015  deranglem  23104  subfacp1lem6  23123  subfacval2  23125  cvmlift2lem12  23252  relexpsucr  23433  relexpsucl  23435  relexprel  23438  relexpdm  23439  relexprn  23440  relexpadd  23442  relexpindlem  23443  relexpind  23444  rtrclreclem.trans  23450  rtrclreclem.min  23451  dfrtrcl2  23452  rtrclind  23453  dfon2lem6  23548  rdgprc  23555  predpoirr  23601  predfrirr  23602  trpredlem1  23634  wfrlem14  23673  frrlem5e  23693  axdenselem8  23746  axsegconlem1  23955  ax5seglem4  23970  ax5seglem5  23971  axlowdimlem15  23994  axcontlem2  24003  axcontlem4  24005  ifscgr  24077  btwncolinear1  24102  hfelhf  24221  ordcmp  24296  findreccl  24302  nndivlub  24307  inpws1  24452  cnveq3  24527  relinccppr  24540  repfuntw  24571  cbcpcp  24573  prl2  24580  dupre2  24655  sege  24663  mxlmnl2  24681  defse3  24683  ablocomgrp  24753  grpodrcan  24786  ltrooo  24815  rltrooo  24826  glmrngo  24893  intopcoaconlem3b  24949  intopcoaconlem3  24950  islimrs4  24993  iint  25023  lvsovso  25037  cnegvex2  25071  rnegvex2  25072  issubcv  25081  isucv  25088  ismulcv  25092  intvconlem1  25114  propsrc  25279  fnctartar  25318  fnctartar2  25319  prismorcset2  25329  isgraphmrph2  25335  domcatsetval2  25340  domcatval2  25342  codcatval2  25348  prismorcset3  25349  idcatval2  25355  domidmor2  25360  codidmor2  25362  grphidmor2  25364  cmp2morpcats  25372  cmp2morpcatt  25373  cmpmor  25386  setiscat  25390  indcls2  25407  empklst  25420  clscnc  25421  cndpv  25460  pgapspf2  25464  lineval12a  25495  lineval2a  25496  lineval2b  25497  sgplpte21d1  25550  sgplpte21d2  25551  segline  25552  xsyysx  25556  bsstrs  25557  nbssntrs  25558  segray  25566  rayline  25567  pdiveql  25579  opnrebl2  25647  nn0prpw  25650  eqfnun  25798  sdclem2  25863  sdclem1  25864  prdsbnd2  25930  ismtyval  25935  rrnequiv  25970  exidreslem  25978  risci  26029  prtlem11  26145  prtlem15  26154  aovmpt4g  27452  bnj168  28037  bnj535  28201  bnj590  28221  bnj594  28223  bnj938  28248  bnj1118  28293  bnj1128  28299  ax10lem17ALT  28402  ax9lem17  28435  cvrat4  28911  lcfl6  30969
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