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

Theorem syl5ibr 234
Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)
Hypotheses
Ref Expression
syl5ibr.1 (𝜑𝜃)
syl5ibr.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5ibr (𝜒 → (𝜑𝜓))

Proof of Theorem syl5ibr
StepHypRef Expression
1 syl5ibr.1 . 2 (𝜑𝜃)
2 syl5ibr.2 . . 3 (𝜒 → (𝜓𝜃))
32bicomd 211 . 2 (𝜒 → (𝜃𝜓))
41, 3syl5ib 232 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  syl5ibrcom  235  biimprd  236  exdistrf  2320  pm2.61ne  2866  unineq  3835  elpreqprlem  4328  oteqex  4883  elopabr  4927  otel3xp  5067  eqrelrdv2  5131  breldmg  5239  elrnmpt1  5282  cnveqb  5494  cnveq0  5495  predpoirr  5611  predfrirr  5612  ordtri3OLD  5663  limelon  5691  ndmfv  6113  ffvresb  6286  isomin  6465  isofrlem  6468  caovord3d  6719  eldifpw  6845  ssonuni  6855  onsucuni2  6903  ordzsl  6914  tfindsg  6929  findsg  6962  oteqimp  7055  frxp  7151  poxp  7153  fnwelem  7156  suppss  7189  wfrlem14  7292  tfrlem11  7348  oacl  7479  omcl  7480  oecl  7481  oa0r  7482  om0r  7483  om1r  7487  oe1m  7489  oaordi  7490  oawordri  7494  oaass  7505  oarec  7506  omwordri  7516  odi  7523  omass  7524  oewordri  7536  oeworde  7537  oeordsuc  7538  oelim2  7539  oeoa  7541  oeoelem  7542  oeoe  7543  nnm0r  7554  nnacl  7555  nnacom  7561  nnaordi  7562  nnaass  7566  nndi  7567  nnmass  7568  nnmsucr  7569  nnmcom  7570  omabs  7591  brecop  7704  eceqoveq  7717  elpm2r  7738  map0g  7760  undifixp  7807  fundmen  7893  mapxpen  7988  mapunen  7991  php  8006  unxpdomlem2  8027  pssnn  8040  f1vrnfibi  8111  elfir  8181  wemapso2lem  8317  wdompwdom  8343  inf3lem1  8385  inf3lem3  8387  cantnfval2  8426  cantnfp1lem3  8437  r1sdom  8497  r1tr  8499  carden2a  8652  fidomtri2  8680  prdom2  8689  infxpenlem  8696  acndom  8734  fodomacn  8739  wdomfil  8744  alephon  8752  alephordi  8757  alephle  8771  alephfplem3  8789  dfac2a  8812  kmlem9  8840  cflm  8932  cfslb  8948  cfslbn  8949  infpssrlem3  8987  infpssrlem4  8988  fin23lem21  9021  fin23lem30  9024  isf34lem7  9061  isf34lem6  9062  fin67  9077  isfin7-2  9078  fin1a2lem7  9088  fin1a2lem10  9091  iundom2g  9218  konigthlem  9246  alephreg  9260  gchdomtri  9307  wunr1om  9397  tskr1om  9445  inar1  9453  grur1a  9497  indpi  9585  genpprecl  9679  genpnmax  9685  addcmpblnr  9746  recexsrlem  9780  map2psrpr  9787  ax1rid  9838  axpre-mulgt0  9845  ltle  9977  nnmulcl  10890  nnsub  10906  nn0sub  11190  nneo  11293  uz11  11542  xrltle  11817  xltnegi  11880  xrsupsslem  11965  xrinfmsslem  11966  xrub  11970  supxrunb1  11977  supxrunb2  11978  om2uzuzi  12565  uzrdgxfr  12583  seqcl2  12636  seqfveq2  12640  seqshft2  12644  seqsplit  12651  seqcaopr3  12653  seqf1olem2a  12656  seqid2  12664  seqhomo  12665  ser1const  12674  m1expcl2  12699  expadd  12719  expmul  12722  faclbnd  12894  hashfzp1  13030  hashmap  13034  hashfacen  13047  hashf1lem1  13048  hashf1lem2  13049  hashf1  13050  seqcoll  13057  wrdsymb0  13140  swrdnd2  13231  wrd2ind  13275  swrdccatin12lem2  13286  swrdccatin1d  13296  repswccat  13329  repswcshw  13355  cshwcshid  13370  rtrclreclem3  13594  rtrclreclem4  13595  dfrtrcl2  13596  relexpindlem  13597  relexpind  13598  rtrclind  13599  recan  13870  rexanre  13880  rlimcn2  14115  caurcvg2  14202  fsumiun  14340  pwm1geoser  14385  efexp  14616  rpnnen2lem12  14739  dvdstr  14802  alzdvds  14826  zob  14867  sumeven  14894  sumodd  14895  bitsinv1  14948  smu01lem  14991  smupval  14994  smueqlem  14996  smumullem  14998  seq1st  15068  lcmfunsnlem2lem1  15135  lcmfunsnlem2lem2  15136  cncongr2  15166  prmdiveq  15275  odzdvds  15284  pythagtriplem2  15306  pcexp  15348  vdwlem13  15481  ramz  15513  prmolefac  15534  elrestr  15858  xpsff1o  15997  subsubc  16282  clatl  16885  frmdgsum  17168  dfgrp3e  17284  mulgneg2  17344  mulgnnass  17345  mulgnnassOLD  17346  mhmmulg  17352  gsumwrev  17565  symgbas  17569  symgextf1lem  17609  symgfixelsi  17624  pmtrdifellem4  17668  sylow1lem1  17782  efgsfo  17921  efgred  17930  cyggexb  18069  gsumzres  18079  gsum2dlem2  18139  ringadd2  18344  mulgass2  18370  lmodprop2d  18694  lspsnne2  18885  lspsneu  18890  assapropd  19094  mplcoe1  19232  mplcoe3  19233  mplcoe5  19235  ply1sclf1  19426  cnfldmulg  19543  cnfldexp  19544  zrhpsgnelbas  19704  mat1scmat  20106  restopn2  20733  cnpf2  20806  cmpfi  20963  txcn  21181  txlm  21203  xkoptsub  21209  xkopjcn  21211  ufildr  21487  cnflf  21558  fclsnei  21575  fclscmp  21586  ufilcmp  21588  cnfcf  21598  symgtgp  21657  isxms2  22004  met2ndc  22079  metustbl  22122  tngngp2  22204  clmmulg  22640  iscau4  22803  ovolunlem1a  22988  ovolicc2lem4  23012  volfiniun  23039  voliunlem1  23042  volsup  23048  dvnadd  23415  dvnres  23417  dvcobr  23432  ply1nzb  23603  plypf1  23689  dgrle  23720  coeaddlem  23726  dgrlt  23743  dvntaylp  23846  cxpmul2  24152  rlimcnp  24409  facgam  24509  wilthlem2  24512  isnsqf  24578  musum  24634  chtub  24654  chpval2  24660  gausslemma2dlem0i  24806  dchrisumlem1  24895  qabvexp  25032  ostthlem2  25034  axsegconlem1  25515  ax5seglem4  25530  ax5seglem5  25531  axlowdimlem15  25554  axcontlem2  25563  axcontlem4  25565  ushgrauhgra  25598  usgra2edg  25677  cusgrafilem1  25773  sizeusglecusglem1  25778  sizeusglecusg  25780  trliswlk  25835  2trllemF  25845  constr3lem6  25943  1conngra  25969  wlkiswwlk2lem4  25988  wwlknredwwlkn0  26021  wwlkextwrd  26022  wwlkextproplem1  26035  wwlkextprop  26038  clwlkisclwwlklem2a  26079  clwwlkf1  26090  erclwwlksym  26108  eleclclwwlknlem2  26112  erclwwlknsym  26120  el2wlkonot  26162  el2spthonot  26163  hashnbgravdg  26206  eupatrl  26261  frgra3vlem1  26293  3vfriswmgralem  26297  frconngra  26314  frgrawopreglem3  26339  frg2wot1  26350  2spotiundisj  26355  usg2spot2nb  26358  usgreg2spot  26360  extwwlkfablem2  26371  numclwwlkovf2ex  26379  extwwlkfab  26383  sspval  26766  nmosetre  26809  nmobndseqi  26824  nmobndseqiALT  26825  orthcom  27155  shsva  27369  shmodsi  27438  h1datomi  27630  nmopsetretALT  27912  nmfnsetre  27926  lnopcnbd  28085  pjclem4  28248  pj3si  28256  ssmd1  28360  atom1d  28402  chjatom  28406  atcvat4i  28446  cdj3lem2a  28485  cdj3lem3a  28488  disjunsn  28595  unitdivcld  29081  xrge0iifiso  29115  dya2iocuni  29478  bnj168  29858  bnj535  30020  bnj590  30040  bnj594  30042  bnj938  30067  bnj1118  30112  bnj1128  30118  deranglem  30208  subfacp1lem6  30227  subfacval2  30229  cvmlift2lem12  30356  mrsubvrs  30479  msrrcl  30500  mclsax  30526  dfon2lem6  30743  rdgprc  30750  trpredlem1  30777  frrlem5e  30838  nodenselem8  30893  ifscgr  31127  btwncolinear1  31152  hfelhf  31264  opnrebl2  31292  nn0prpw  31294  ordcmp  31422  findreccl  31428  nndivlub  31433  bj-rest0  32023  topdifinffinlem  32167  iooelexlt  32182  rdgeqoa  32190  wl-mo3t  32333  matunitlindflem2  32372  poimirlem2  32377  poimirlem23  32398  poimirlem28  32403  poimirlem29  32404  poimirlem31  32406  poimirlem32  32407  eqfnun  32482  sdclem2  32504  sdclem1  32505  prdsbnd2  32560  ismtyval  32565  rrnequiv  32600  isexid2  32620  ismndo1  32638  exidreslem  32642  rngo2  32672  rngoueqz  32705  risci  32752  prtlem11  32965  prtlem15  32974  cvrat4  33543  lcfl6  35603  clcnvlem  36745  cnvrcl0  36747  cnvtrcl0  36748  iunrelexpmin1  36815  iunrelexpmin2  36819  aovmpt4g  39728  iccpartiltu  39758  iccpartgt  39763  iccpartgel  39765  fmtnofac1  39818  gbepos  39978  pfxccatin12lem2  40085  f1ssf1  40140  incistruhgr  40300  upgredg2vtx  40368  upgredgpr  40369  uhgr2edg  40430  nbupgruvtxres  40629  cusgrfilem1  40666  1wlkres  40874  1wlkp1lem2  40878  pthdivtx  40930  pthdlem2lem  40968  1wlkiswwlks2lem4  41064  wwlksnredwwlkn0  41097  wwlksnextwrd  41098  wwlksnextprop  41113  wwlksnonfi  41122  clwlkclwwlklem2a  41202  clwwlksf1  41219  erclwwlkssym  41237  eleclclwwlksnlem2  41241  erclwwlksnsym  41249  eupth2lem3lem6  41396  frgr3vlem1  41438  3vfriswmgrlem  41442  frgr2wwlk1  41489  av-numclwwlkovf2ex  41512  av-extwwlkfab  41515  funcrngcsetc  41785  funcrngcsetcALT  41786  rhmsscrnghm  41813  funcringcsetc  41822  ellcoellss  42013  dignn0flhalflem2  42203  nn0sumshdiglemB  42207
  Copyright terms: Public domain W3C validator