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  2523  unineq  3421  oteqex  4261  ordtri3  4430  limelon  4457  eldifpw  4568  ssonuni  4580  onsucuni2  4627  ordzsl  4638  tfindsg  4653  findsg  4685  elrnmpt1  4930  cnveqb  5131  cnveq0  5132  relcoi1  5203  ndmfv  5554  ffvresb  5692  isomin  5836  isofrlem  5839  caovord3d  6032  frxp  6227  poxp  6229  fnwelem  6232  tfrlem1  6393  tfrlem11  6406  oacl  6536  omcl  6537  oecl  6538  oa0r  6539  om0r  6540  om1r  6543  oe1m  6545  oaordi  6546  oawordri  6550  oaass  6561  oarec  6562  omwordri  6572  odi  6579  omass  6580  oewordri  6592  oeworde  6593  oeordsuc  6594  oelim2  6595  oeoa  6597  oeoelem  6598  oeoe  6599  nnm0r  6610  nnacl  6611  nnacom  6617  nnaordi  6618  nnaass  6622  nndi  6623  nnmass  6624  nnmsucr  6625  nnmcom  6626  omabs  6647  brecop  6753  eceqoveq  6765  elpm2r  6790  map0g  6809  undifixp  6854  fundmen  6936  mapxpen  7029  mapunen  7032  php  7047  unxpdomlem2  7070  pssnn  7083  elfir  7171  wemapso2  7269  wdompwdom  7294  inf3lem1  7331  inf3lem3  7333  noinfepOLD  7363  cantnfval2  7372  cantnfp1lem3  7384  r1sdom  7448  r1tr  7450  carden2a  7601  fidomtri2  7629  prdom2  7638  infxpenlem  7643  acndom  7680  fodomacn  7685  wdomfil  7690  alephon  7698  alephordi  7703  alephle  7717  alephfplem3  7735  dfac2a  7758  kmlem9  7786  cflm  7878  cfslb  7894  cfslbn  7895  infpssrlem3  7933  infpssrlem4  7934  fin23lem21  7967  fin23lem30  7970  isf34lem7  8007  isf34lem6  8008  fin67  8023  isfin7-2  8024  fin1a2lem7  8034  fin1a2lem10  8037  iundom2g  8164  konigthlem  8192  alephreg  8206  gchdomtri  8253  wunr1om  8343  tskr1om  8391  inar1  8399  grur1a  8443  indpi  8533  genpprecl  8627  genpnmax  8633  addcmpblnr  8696  recexsrlem  8727  map2psrpr  8734  ax1rid  8785  axpre-mulgt0  8792  ltle  8912  nnmulcl  9771  nnsub  9786  nn0sub  10016  nneo  10097  uzindOLD  10108  uz11  10252  xrltle  10485  xltnegi  10545  xrsupsslem  10627  xrinfmsslem  10628  xrub  10632  supxrunb1  10640  supxrunb2  10641  om2uzuzi  11014  uzrdgxfr  11031  seqcl2  11066  seqfveq2  11070  seqshft2  11074  seqsplit  11081  seqcaopr3  11083  seqf1olem2a  11086  seqid2  11094  seqhomo  11095  ser1const  11104  m1expcl2  11127  expadd  11146  expmul  11149  faclbnd  11305  hashmap  11389  hashfacen  11394  hashf1lem1  11395  hashf1lem2  11396  hashf1  11397  seqcoll  11403  recan  11822  rexanre  11832  rlimcn2  12066  caurcvg2  12152  fsumiun  12281  efexp  12383  rpnnen2  12506  dvdstr  12564  alzdvds  12580  bitsinv1  12635  smu01lem  12678  smupval  12681  smueqlem  12683  smumullem  12685  seq1st  12743  prmdiveq  12856  odzdvds  12862  pythagtriplem2  12872  pcexp  12914  vdwlem13  13042  ramz  13074  elrestr  13335  xpsff1o  13472  subsubc  13729  frmdgsum  14486  mulgneg2  14596  mulgnnass  14597  mhmmulg  14601  symgbas  14774  gsumwrev  14841  sylow1lem1  14911  efgsfo  15050  efgred  15059  cyggexb  15187  gsum2d  15225  mulgass2  15389  lmodprop2d  15689  lspsnne2  15873  lspsneu  15878  assapropd  16069  mplcoe1  16211  mplcoe3  16212  mplcoe2  16213  ply1sclf1  16366  cnfldmulg  16408  cnfldexp  16409  restopn2  16910  cnpf2  16982  cmpfi  17137  txcn  17322  txlm  17344  xkoptsub  17350  xkopjcn  17352  ufildr  17628  cnflf  17699  fclsnei  17716  fclscmp  17727  ufilcmp  17729  cnfcf  17739  symgtgp  17786  isxms2  17996  met2ndc  18071  tngngp2  18170  clmmulg  18593  iscau4  18707  ovolunlem1a  18857  ovolicc2lem4  18881  volfiniun  18906  voliunlem1  18909  volsup  18915  dvnadd  19280  dvnres  19282  dvcobr  19297  ply1nzb  19510  plypf1  19596  dgrle  19627  coeaddlem  19632  dgrlt  19649  dvntaylp  19752  cxpmul2  20038  rlimcnp  20262  wilthlem2  20309  isnsqf  20375  musum  20433  chtub  20453  chpval2  20459  dchrisumlem1  20640  qabvexp  20777  ostthlem2  20779  isexid2  20994  ismndo1  21013  rngo2  21057  rngoueqz  21099  sspval  21301  nmosetre  21344  nmobndseqi  21359  nmobndseqiOLD  21360  orthcom  21689  shsva  21901  shmodsi  21970  h1datomi  22162  nmopsetretALT  22445  nmfnsetre  22459  lnopcnbd  22618  pjclem4  22781  pj3si  22789  ssmd1  22893  atom1d  22935  chjatom  22939  atcvat4i  22979  cdj3lem2a  23018  cdj3lem3a  23021  deranglem  23699  subfacp1lem6  23718  subfacval2  23720  cvmlift2lem12  23847  relexpsucr  24028  relexpsucl  24030  relexprel  24033  relexpdm  24034  relexprn  24035  relexpadd  24037  relexpindlem  24038  relexpind  24039  rtrclreclem.trans  24045  rtrclreclem.min  24046  dfrtrcl2  24047  rtrclind  24048  dfon2lem6  24146  rdgprc  24153  predpoirr  24199  predfrirr  24200  trpredlem1  24232  wfrlem14  24271  frrlem5e  24291  nodenselem8  24344  axsegconlem1  24547  ax5seglem4  24562  ax5seglem5  24563  axlowdimlem15  24586  axcontlem2  24595  axcontlem4  24597  ifscgr  24669  btwncolinear1  24694  hfelhf  24813  ordcmp  24888  findreccl  24894  nndivlub  24899  inpws1  25053  relinccppr  25140  cbcpcp  25173  prl2  25180  dupre2  25255  sege  25263  mxlmnl2  25281  defse3  25283  ablocomgrp  25353  grpodrcan  25386  ltrooo  25415  rltrooo  25426  glmrngo  25493  intopcoaconlem3b  25549  intopcoaconlem3  25550  islimrs4  25593  iint  25623  lvsovso  25637  cnegvex2  25671  rnegvex2  25672  issubcv  25681  isucv  25688  ismulcv  25692  intvconlem1  25714  propsrc  25879  fnctartar  25918  fnctartar2  25919  prismorcset2  25929  isgraphmrph2  25935  domcatsetval2  25940  domcatval2  25942  codcatval2  25948  prismorcset3  25949  idcatval2  25955  domidmor2  25960  codidmor2  25962  grphidmor2  25964  cmp2morpcats  25972  cmp2morpcatt  25973  cmpmor  25986  setiscat  25990  indcls2  26007  empklst  26020  clscnc  26021  cndpv  26060  pgapspf2  26064  lineval12a  26095  lineval2a  26096  lineval2b  26097  sgplpte21d1  26150  sgplpte21d2  26151  segline  26152  xsyysx  26156  bsstrs  26157  nbssntrs  26158  segray  26166  rayline  26167  pdiveql  26179  opnrebl2  26247  nn0prpw  26250  eqfnun  26398  sdclem2  26463  sdclem1  26464  prdsbnd2  26530  ismtyval  26535  rrnequiv  26570  exidreslem  26578  risci  26629  prtlem11  26745  prtlem15  26754  aovmpt4g  28072  nbusgra  28154  frgra3vlem1  28189  3vfriswmgralem  28193  bnj168  28831  bnj535  28995  bnj590  29015  bnj594  29017  bnj938  29042  bnj1118  29087  bnj1128  29093  ax10lem17ALT  29196  ax9lem17  29229  cvrat4  29705  lcfl6  31763
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