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  1879  pm2.61ne  2521  unineq  3419  oteqex  4259  ordtri3  4428  limelon  4455  eldifpw  4566  ssonuni  4578  onsucuni2  4625  ordzsl  4636  tfindsg  4651  findsg  4683  elrnmpt1  4928  cnveqb  5129  cnveq0  5130  relcoi1  5201  ndmfv  5552  ffvresb  5690  isomin  5834  isofrlem  5837  caovord3d  6030  frxp  6225  poxp  6227  fnwelem  6230  tfrlem1  6391  tfrlem11  6404  oacl  6534  omcl  6535  oecl  6536  oa0r  6537  om0r  6538  om1r  6541  oe1m  6543  oaordi  6544  oawordri  6548  oaass  6559  oarec  6560  omwordri  6570  odi  6577  omass  6578  oewordri  6590  oeworde  6591  oeordsuc  6592  oelim2  6593  oeoa  6595  oeoelem  6596  oeoe  6597  nnm0r  6608  nnacl  6609  nnacom  6615  nnaordi  6616  nnaass  6620  nndi  6621  nnmass  6622  nnmsucr  6623  nnmcom  6624  omabs  6645  brecop  6751  eceqoveq  6763  elpm2r  6788  map0g  6807  undifixp  6852  fundmen  6934  mapxpen  7027  mapunen  7030  php  7045  unxpdomlem2  7068  pssnn  7081  elfir  7169  wemapso2  7267  wdompwdom  7292  inf3lem1  7329  inf3lem3  7331  noinfepOLD  7361  cantnfval2  7370  cantnfp1lem3  7382  r1sdom  7446  r1tr  7448  carden2a  7599  fidomtri2  7627  prdom2  7636  infxpenlem  7641  acndom  7678  fodomacn  7683  wdomfil  7688  alephon  7696  alephordi  7701  alephle  7715  alephfplem3  7733  dfac2a  7756  kmlem9  7784  cflm  7876  cfslb  7892  cfslbn  7893  infpssrlem3  7931  infpssrlem4  7932  fin23lem21  7965  fin23lem30  7968  isf34lem7  8005  isf34lem6  8006  fin67  8021  isfin7-2  8022  fin1a2lem7  8032  fin1a2lem10  8035  iundom2g  8162  konigthlem  8190  alephreg  8204  gchdomtri  8251  wunr1om  8341  tskr1om  8389  inar1  8397  grur1a  8441  indpi  8531  genpprecl  8625  genpnmax  8631  addcmpblnr  8694  recexsrlem  8725  map2psrpr  8732  ax1rid  8783  axpre-mulgt0  8790  ltle  8910  nnmulcl  9769  nnsub  9784  nn0sub  10014  nneo  10095  uzindOLD  10106  uz11  10250  xrltle  10483  xltnegi  10543  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  supxrunb1  10638  supxrunb2  10639  om2uzuzi  11012  uzrdgxfr  11029  seqcl2  11064  seqfveq2  11068  seqshft2  11072  seqsplit  11079  seqcaopr3  11081  seqf1olem2a  11084  seqid2  11092  seqhomo  11093  ser1const  11102  m1expcl2  11125  expadd  11144  expmul  11147  faclbnd  11303  hashmap  11387  hashfacen  11392  hashf1lem1  11393  hashf1lem2  11394  hashf1  11395  seqcoll  11401  recan  11820  rexanre  11830  rlimcn2  12064  caurcvg2  12150  fsumiun  12279  efexp  12381  rpnnen2  12504  dvdstr  12562  alzdvds  12578  bitsinv1  12633  smu01lem  12676  smupval  12679  smueqlem  12681  smumullem  12683  seq1st  12741  prmdiveq  12854  odzdvds  12860  pythagtriplem2  12870  pcexp  12912  vdwlem13  13040  ramz  13072  elrestr  13333  xpsff1o  13470  subsubc  13727  frmdgsum  14484  mulgneg2  14594  mulgnnass  14595  mhmmulg  14599  symgbas  14772  gsumwrev  14839  sylow1lem1  14909  efgsfo  15048  efgred  15057  cyggexb  15185  gsum2d  15223  mulgass2  15387  lmodprop2d  15687  lspsnne2  15871  lspsneu  15876  assapropd  16067  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  ply1sclf1  16364  cnfldmulg  16406  cnfldexp  16407  restopn2  16908  cnpf2  16980  cmpfi  17135  txcn  17320  txlm  17342  xkoptsub  17348  xkopjcn  17350  ufildr  17626  cnflf  17697  fclsnei  17714  fclscmp  17725  ufilcmp  17727  cnfcf  17737  symgtgp  17784  isxms2  17994  met2ndc  18069  tngngp2  18168  clmmulg  18591  iscau4  18705  ovolunlem1a  18855  ovolicc2lem4  18879  volfiniun  18904  voliunlem1  18907  volsup  18913  dvnadd  19278  dvnres  19280  dvcobr  19295  ply1nzb  19508  plypf1  19594  dgrle  19625  coeaddlem  19630  dgrlt  19647  dvntaylp  19750  cxpmul2  20036  rlimcnp  20260  wilthlem2  20307  isnsqf  20373  musum  20431  chtub  20451  chpval2  20457  dchrisumlem1  20638  qabvexp  20775  ostthlem2  20777  isexid2  20992  ismndo1  21011  rngo2  21055  rngoueqz  21097  sspval  21299  nmosetre  21342  nmobndseqi  21357  nmobndseqiOLD  21358  orthcom  21687  shsva  21899  shmodsi  21968  h1datomi  22160  nmopsetretALT  22443  nmfnsetre  22457  lnopcnbd  22616  pjclem4  22779  pj3si  22787  ssmd1  22891  atom1d  22933  chjatom  22937  atcvat4i  22977  cdj3lem2a  23016  cdj3lem3a  23019  deranglem  23697  subfacp1lem6  23716  subfacval2  23718  cvmlift2lem12  23845  relexpsucr  24026  relexpsucl  24028  relexprel  24031  relexpdm  24032  relexprn  24033  relexpadd  24035  relexpindlem  24036  relexpind  24037  rtrclreclem.trans  24043  rtrclreclem.min  24044  dfrtrcl2  24045  rtrclind  24046  dfon2lem6  24144  rdgprc  24151  predpoirr  24197  predfrirr  24198  trpredlem1  24230  wfrlem14  24269  frrlem5e  24289  nodenselem8  24342  axsegconlem1  24545  ax5seglem4  24560  ax5seglem5  24561  axlowdimlem15  24584  axcontlem2  24593  axcontlem4  24595  ifscgr  24667  btwncolinear1  24692  hfelhf  24811  ordcmp  24886  findreccl  24892  nndivlub  24897  inpws1  25042  relinccppr  25129  cbcpcp  25162  prl2  25169  dupre2  25244  sege  25252  mxlmnl2  25270  defse3  25272  ablocomgrp  25342  grpodrcan  25375  ltrooo  25404  rltrooo  25415  glmrngo  25482  intopcoaconlem3b  25538  intopcoaconlem3  25539  islimrs4  25582  iint  25612  lvsovso  25626  cnegvex2  25660  rnegvex2  25661  issubcv  25670  isucv  25677  ismulcv  25681  intvconlem1  25703  propsrc  25868  fnctartar  25907  fnctartar2  25908  prismorcset2  25918  isgraphmrph2  25924  domcatsetval2  25929  domcatval2  25931  codcatval2  25937  prismorcset3  25938  idcatval2  25944  domidmor2  25949  codidmor2  25951  grphidmor2  25953  cmp2morpcats  25961  cmp2morpcatt  25962  cmpmor  25975  setiscat  25979  indcls2  25996  empklst  26009  clscnc  26010  cndpv  26049  pgapspf2  26053  lineval12a  26084  lineval2a  26085  lineval2b  26086  sgplpte21d1  26139  sgplpte21d2  26140  segline  26141  xsyysx  26145  bsstrs  26146  nbssntrs  26147  segray  26155  rayline  26156  pdiveql  26168  opnrebl2  26236  nn0prpw  26239  eqfnun  26387  sdclem2  26452  sdclem1  26453  prdsbnd2  26519  ismtyval  26524  rrnequiv  26559  exidreslem  26567  risci  26618  prtlem11  26734  prtlem15  26743  aovmpt4g  28061  nbusgra  28143  frgra3vlem1  28178  3vfriswmgralem  28182  bnj168  28758  bnj535  28922  bnj590  28942  bnj594  28944  bnj938  28969  bnj1118  29014  bnj1128  29020  ax10lem17ALT  29123  ax9lem17  29156  cvrat4  29632  lcfl6  31690
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