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

Theorem syl5ibr 213
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 193 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 211 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  syl5ibrcom  214  biimprd  215  dvelimvOLD  1994  pm2.61ne  2642  unineq  3551  oteqex  4409  ordtri3  4577  limelon  4604  eldifpw  4714  ssonuni  4726  onsucuni2  4773  ordzsl  4784  tfindsg  4799  findsg  4831  elrnmpt1  5078  cnveqb  5285  cnveq0  5286  relcoi1  5357  ndmfv  5714  ffvresb  5859  isomin  6016  isofrlem  6019  caovord3d  6216  frxp  6415  poxp  6417  fnwelem  6420  tfrlem1  6595  tfrlem11  6608  oacl  6738  omcl  6739  oecl  6740  oa0r  6741  om0r  6742  om1r  6745  oe1m  6747  oaordi  6748  oawordri  6752  oaass  6763  oarec  6764  omwordri  6774  odi  6781  omass  6782  oewordri  6794  oeworde  6795  oeordsuc  6796  oelim2  6797  oeoa  6799  oeoelem  6800  oeoe  6801  nnm0r  6812  nnacl  6813  nnacom  6819  nnaordi  6820  nnaass  6824  nndi  6825  nnmass  6826  nnmsucr  6827  nnmcom  6828  omabs  6849  brecop  6956  eceqoveq  6968  elpm2r  6993  map0g  7012  undifixp  7057  fundmen  7139  mapxpen  7232  mapunen  7235  php  7250  unxpdomlem2  7273  pssnn  7286  elfir  7378  wemapso2  7477  wdompwdom  7502  inf3lem1  7539  inf3lem3  7541  noinfepOLD  7571  cantnfval2  7580  cantnfp1lem3  7592  r1sdom  7656  r1tr  7658  carden2a  7809  fidomtri2  7837  prdom2  7846  infxpenlem  7851  acndom  7888  fodomacn  7893  wdomfil  7898  alephon  7906  alephordi  7911  alephle  7925  alephfplem3  7943  dfac2a  7966  kmlem9  7994  cflm  8086  cfslb  8102  cfslbn  8103  infpssrlem3  8141  infpssrlem4  8142  fin23lem21  8175  fin23lem30  8178  isf34lem7  8215  isf34lem6  8216  fin67  8231  isfin7-2  8232  fin1a2lem7  8242  fin1a2lem10  8245  iundom2g  8371  konigthlem  8399  alephreg  8413  gchdomtri  8460  wunr1om  8550  tskr1om  8598  inar1  8606  grur1a  8650  indpi  8740  genpprecl  8834  genpnmax  8840  addcmpblnr  8903  recexsrlem  8934  map2psrpr  8941  ax1rid  8992  axpre-mulgt0  8999  ltle  9119  nnmulcl  9979  nnsub  9994  nn0sub  10226  nneo  10309  uzindOLD  10320  uz11  10464  xrltle  10698  xltnegi  10758  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  supxrunb1  10854  supxrunb2  10855  om2uzuzi  11244  uzrdgxfr  11261  seqcl2  11296  seqfveq2  11300  seqshft2  11304  seqsplit  11311  seqcaopr3  11313  seqf1olem2a  11316  seqid2  11324  seqhomo  11325  ser1const  11334  m1expcl2  11358  expadd  11377  expmul  11380  faclbnd  11536  hashmap  11653  hashfacen  11658  hashf1lem1  11659  hashf1lem2  11660  hashf1  11661  seqcoll  11667  recan  12095  rexanre  12105  rlimcn2  12339  caurcvg2  12426  fsumiun  12555  efexp  12657  rpnnen2  12780  dvdstr  12838  alzdvds  12854  bitsinv1  12909  smu01lem  12952  smupval  12955  smueqlem  12957  smumullem  12959  seq1st  13017  prmdiveq  13130  odzdvds  13136  pythagtriplem2  13146  pcexp  13188  vdwlem13  13316  ramz  13348  elrestr  13611  xpsff1o  13748  subsubc  14005  frmdgsum  14762  mulgneg2  14872  mulgnnass  14873  mhmmulg  14877  symgbas  15050  gsumwrev  15117  sylow1lem1  15187  efgsfo  15326  efgred  15335  cyggexb  15463  gsum2d  15501  mulgass2  15665  lmodprop2d  15961  lspsnne2  16145  lspsneu  16150  assapropd  16341  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  ply1sclf1  16635  cnfldmulg  16688  cnfldexp  16689  restopn2  17195  cnpf2  17268  cmpfi  17425  txcn  17611  txlm  17633  xkoptsub  17639  xkopjcn  17641  ufildr  17916  cnflf  17987  fclsnei  18004  fclscmp  18015  ufilcmp  18017  cnfcf  18027  symgtgp  18084  isxms2  18431  met2ndc  18506  metustblOLD  18563  metustbl  18564  tngngp2  18646  clmmulg  19071  iscau4  19185  ovolunlem1a  19345  ovolicc2lem4  19369  volfiniun  19394  voliunlem1  19397  volsup  19403  dvnadd  19768  dvnres  19770  dvcobr  19785  ply1nzb  19998  plypf1  20084  dgrle  20115  coeaddlem  20120  dgrlt  20137  dvntaylp  20240  cxpmul2  20533  rlimcnp  20757  wilthlem2  20805  isnsqf  20871  musum  20929  chtub  20949  chpval2  20955  dchrisumlem1  21136  qabvexp  21273  ostthlem2  21275  usgra2edg  21355  cusgrafilem1  21441  sizeusglecusglem1  21446  sizeusglecusg  21448  trliswlk  21492  2trllemF  21502  constr3lem6  21589  1conngra  21615  hashnbgravdg  21635  eupatrl  21643  isexid2  21866  ismndo1  21885  rngo2  21929  rngoueqz  21971  sspval  22175  nmosetre  22218  nmobndseqi  22233  nmobndseqiOLD  22234  orthcom  22563  shsva  22775  shmodsi  22844  h1datomi  23036  nmopsetretALT  23319  nmfnsetre  23333  lnopcnbd  23492  pjclem4  23655  pj3si  23663  ssmd1  23767  atom1d  23809  chjatom  23813  atcvat4i  23853  cdj3lem2a  23892  cdj3lem3a  23895  unitdivcld  24252  xrge0iifiso  24274  dya2iocuni  24586  facgam  24803  deranglem  24805  subfacp1lem6  24824  subfacval2  24826  cvmlift2lem12  24954  relexpsucr  25083  relexpsucl  25085  relexprel  25087  relexpdm  25088  relexprn  25089  relexpadd  25091  relexpindlem  25092  relexpind  25093  rtrclreclem.trans  25099  rtrclreclem.min  25100  dfrtrcl2  25101  rtrclind  25102  dfon2lem6  25358  rdgprc  25365  predpoirr  25411  predfrirr  25412  trpredlem1  25444  wfrlem14  25483  frrlem5e  25503  nodenselem8  25556  axsegconlem1  25760  ax5seglem4  25775  ax5seglem5  25776  axlowdimlem15  25799  axcontlem2  25808  axcontlem4  25810  ifscgr  25882  btwncolinear1  25907  hfelhf  26026  ordcmp  26101  findreccl  26107  nndivlub  26112  opnrebl2  26214  nn0prpw  26216  eqfnun  26313  sdclem2  26336  sdclem1  26337  prdsbnd2  26394  ismtyval  26399  rrnequiv  26434  exidreslem  26442  risci  26493  prtlem11  26605  prtlem15  26614  aovmpt4g  27932  otel3xp  27950  oteqimp  27951  swrdccatin2  28018  swrdccatin12lem3  28024  swrdccatin12b  28027  swrdccatin12c  28028  swrdccat3  28029  swrdccat3b  28031  el2wlkonot  28066  el2spthonot  28067  frgra3vlem1  28104  3vfriswmgralem  28108  frconngra  28125  frgrawopreglem3  28149  frg2wot1  28160  2spotiundisj  28165  usg2spot2nb  28168  usgreg2spot  28170  bnj168  28803  bnj535  28967  bnj590  28987  bnj594  28989  bnj938  29014  bnj1118  29059  bnj1128  29065  dvelimvNEW7  29168  cvrat4  29925  lcfl6  31983
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 178
  Copyright terms: Public domain W3C validator