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

Theorem syl5ibr 237
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 214 . 2 (𝜒 → (𝜃𝜓))
41, 3syl5ib 235 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  syl5ibrcom  238  biimprd  239  exdistrf  2497  pm2.61ne  3070  unineq  4086  elpreqprlem  4595  oteqex  5160  elopabr  5215  otel3xp  5360  eqrelrdv2  5428  breldmg  5538  elrnmpt1  5582  cnveqb  5808  cnveq0  5809  predpoirr  5928  predfrirr  5929  limelon  6007  f1ssf1  6387  ndmfv  6441  ffvresb  6619  isomin  6814  isofrlem  6817  caovord3d  7077  eldifpw  7209  ssonuni  7219  onsucuni2  7267  ordzsl  7278  tfindsg  7293  findsg  7326  oteqimp  7420  frxp  7524  poxp  7526  fnwelem  7529  suppss  7563  wfrlem14  7667  tfrlem11  7723  oacl  7855  omcl  7856  oecl  7857  oa0r  7858  om0r  7859  om1r  7863  oe1m  7865  oaordi  7866  oawordri  7870  oaass  7881  oarec  7882  omwordri  7892  odi  7899  omass  7900  oewordri  7912  oeworde  7913  oeordsuc  7914  oelim2  7915  oeoa  7917  oeoelem  7918  oeoe  7919  nnm0r  7930  nnacl  7931  nnacom  7937  nnaordi  7938  nnaass  7942  nndi  7943  nnmass  7944  nnmsucr  7945  nnmcom  7946  omabs  7967  brecop  8078  eceqoveq  8091  elpm2r  8113  map0g  8136  undifixp  8184  fundmen  8269  mapxpen  8368  mapunen  8371  php  8386  unxpdomlem2  8407  pssnn  8420  f1vrnfibi  8493  elfir  8563  wemapso2lem  8699  wdompwdom  8725  inf3lem1  8775  inf3lem3  8777  cantnfval2  8816  cantnfp1lem3  8827  r1sdom  8887  r1tr  8889  carden2a  9078  fidomtri2  9106  prdom2  9115  infxpenlem  9122  acndom  9160  fodomacn  9165  wdomfil  9170  alephon  9178  alephordi  9183  alephle  9197  alephfplem3  9215  dfac2a  9238  kmlem9  9268  cflm  9360  cfslb  9376  cfslbn  9377  infpssrlem3  9415  infpssrlem4  9416  fin23lem21  9449  fin23lem30  9452  isf34lem7  9489  isf34lem6  9490  fin67  9505  isfin7-2  9506  fin1a2lem7  9516  fin1a2lem10  9519  iundom2g  9650  konigthlem  9678  alephreg  9692  gchdomtri  9739  wunr1om  9829  tskr1om  9877  inar1  9885  grur1a  9929  indpi  10017  genpprecl  10111  genpnmax  10117  addcmpblnr  10178  recexsrlem  10212  map2psrpr  10219  ax1rid  10270  axpre-mulgt0  10277  ltle  10414  nnmulcl  11331  nnmulclOLD  11332  nnsub  11348  nn0sub  11612  nneo  11730  uz11  11930  xrltle  12201  xltnegi  12268  xrsupsslem  12358  xrinfmsslem  12359  xrub  12363  supxrunb1  12370  supxrunb2  12371  om2uzuzi  12975  uzrdgxfr  12993  seqcl2  13045  seqfveq2  13049  seqshft2  13053  seqsplit  13060  seqcaopr3  13062  seqf1olem2a  13065  seqid2  13073  seqhomo  13074  ser1const  13083  m1expcl2  13108  expadd  13128  expmul  13131  faclbnd  13300  hashfzp1  13438  hashmap  13442  hashfacen  13458  hashf1lem1  13459  hashf1lem2  13460  hashf1  13461  seqcoll  13468  wrdsymb0  13553  len0nnbi  13555  swrdnd2  13660  wrd2ind  13704  swrdccatin12lem2  13716  swrdccatin1d  13726  repswccat  13759  repswcshw  13785  cshwcshid  13800  rtrclreclem3  14026  rtrclreclem4  14027  dfrtrcl2  14028  relexpindlem  14029  relexpind  14030  rtrclind  14031  recan  14302  rexanre  14312  rlimcn2  14547  caurcvg2  14634  fsumiun  14778  pwm1geoser  14825  efexp  15054  rpnnen2lem12  15177  dvdstr  15244  alzdvds  15268  zob  15306  sumeven  15333  sumodd  15334  bitsinv1  15386  smu01lem  15429  smupval  15432  smueqlem  15434  smumullem  15436  seq1st  15506  lcmfunsnlem2lem1  15573  lcmfunsnlem2lem2  15574  cncongr2  15603  prmdiveq  15711  odzdvds  15720  pythagtriplem2  15742  pcexp  15784  vdwlem13  15917  ramz  15949  prmolefac  15970  elrestr  16297  xpsff1o  16436  subsubc  16720  clatl  17324  frmdgsum  17607  dfgrp3e  17723  mulgneg2  17781  mulgnnass  17782  mhmmulg  17788  gsumwrev  18000  symgbas  18004  symgextf1lem  18044  symgfixelsi  18059  pmtrdifellem4  18103  sylow1lem1  18217  efgsfo  18356  efgred  18365  cyggexb  18504  gsumzres  18514  gsum2dlem2  18574  ringadd2  18780  mulgass2  18806  lmodprop2d  19132  lspsnne2  19328  lspsneu  19333  assapropd  19539  mplcoe1  19677  mplcoe3  19678  mplcoe5  19680  ply1sclf1  19870  cnfldmulg  19989  cnfldexp  19990  zrhpsgnelbas  20151  mat1scmat  20560  restopn2  21199  cnpf2  21272  cmpfi  21429  txcn  21647  txlm  21669  xkoptsub  21675  xkopjcn  21677  ufildr  21952  cnflf  22023  fclsnei  22040  fclscmp  22051  ufilcmp  22053  cnfcf  22063  symgtgp  22122  isxms2  22470  met2ndc  22545  metustbl  22588  tngngp2  22673  clmmulg  23117  iscau4  23294  ovolunlem1a  23483  ovolicc2lem4  23507  volfiniun  23534  voliunlem1  23537  volsup  23543  dvnadd  23912  dvnres  23914  dvcobr  23929  ply1nzb  24102  plypf1  24188  dgrle  24219  coeaddlem  24225  dgrlt  24242  dvntaylp  24345  cxpmul2  24655  rlimcnp  24912  facgam  25012  wilthlem2  25015  isnsqf  25081  musum  25137  chtub  25157  chpval2  25163  gausslemma2dlem0i  25309  dchrisumlem1  25398  qabvexp  25535  ostthlem2  25537  axsegconlem1  26017  ax5seglem4  26032  ax5seglem5  26033  axlowdimlem15  26056  axcontlem2  26065  axcontlem4  26067  incistruhgr  26194  upgredg2vtx  26257  upgredgpr  26258  numedglnl  26260  uhgr2edg  26321  nbupgruvtxres  26536  cusgrfilem1  26585  wlkres  26801  wlkp1lem2  26805  pthdivtx  26859  pthdlem2lem  26897  wlkiswwlks2lem4  27005  wwlksnredwwlkn0  27039  wwlksnextwrd  27040  wwlksnextprop  27056  clwlkclwwlklem2a  27147  clwlkclwwlkf1lem2  27154  erclwwlksym  27170  clwwlkf1  27204  eleclclwwlknlem2  27218  erclwwlknsym  27227  clwwlknonex2  27284  eupth2lem3lem6  27412  frgr3vlem1  27454  3vfriswmgrlem  27458  wlkl0  27553  sspval  27912  nmosetre  27953  nmobndseqi  27968  nmobndseqiALT  27969  orthcom  28299  shsva  28513  shmodsi  28582  h1datomi  28774  nmopsetretALT  29056  nmfnsetre  29070  lnopcnbd  29229  pjclem4  29392  pj3si  29400  ssmd1  29504  atom1d  29546  chjatom  29550  atcvat4i  29590  cdj3lem2a  29629  cdj3lem3a  29632  disjunsn  29738  unitdivcld  30278  xrge0iifiso  30312  dya2iocuni  30676  bnj168  31127  bnj535  31288  bnj590  31308  bnj594  31310  bnj938  31335  bnj1118  31380  bnj1128  31386  deranglem  31476  subfacp1lem6  31495  subfacval2  31497  cvmlift2lem12  31624  mrsubvrs  31747  msrrcl  31768  mclsax  31794  dfon2lem6  32018  rdgprc  32025  trpredlem1  32052  frrlem5e  32114  nodenselem8  32167  slerec  32249  ifscgr  32477  btwncolinear1  32502  hfelhf  32614  opnrebl2  32642  nn0prpw  32644  ordcmp  32768  findreccl  32774  nndivlub  32779  bj-rest0  33359  topdifinffinlem  33513  iooelexlt  33528  rdgeqoa  33536  wl-mo3t  33674  matunitlindflem2  33721  poimirlem2  33726  poimirlem23  33747  poimirlem28  33752  poimirlem29  33753  poimirlem31  33755  poimirlem32  33756  eqfnun  33830  sdclem2  33851  sdclem1  33852  prdsbnd2  33907  ismtyval  33912  rrnequiv  33947  isexid2  33967  ismndo1  33985  exidreslem  33989  rngo2  34019  rngoueqz  34052  risci  34099  prtlem11  34647  prtlem15  34656  cvrat4  35225  lcfl6  37282  clcnvlem  38431  cnvrcl0  38433  cnvtrcl0  38434  iunrelexpmin1  38501  iunrelexpmin2  38505  aovmpt4g  41791  iccpartiltu  41934  iccpartgt  41939  iccpartgel  41941  pfxccatin12lem2  42000  fmtnofac1  42058  gbepos  42222  funcrngcsetc  42567  funcrngcsetcALT  42568  rhmsscrnghm  42595  funcringcsetc  42604  ellcoellss  42793  dignn0flhalflem2  42979  nn0sumshdiglemB  42983
  Copyright terms: Public domain W3C validator