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

Theorem syl3an1 1160
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an1.1 (𝜑𝜓)
syl3an1.2 ((𝜓𝜒𝜃) → 𝜏)
Assertion
Ref Expression
syl3an1 ((𝜑𝜒𝜃) → 𝜏)

Proof of Theorem syl3an1
StepHypRef Expression
1 syl3an1.1 . . 3 (𝜑𝜓)
213anim1i 1149 . 2 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
3 syl3an1.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl 17 1 ((𝜑𝜒𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  3adant1l  1173  3adant1r  1174  syl3an1b  1400  syl3an1br  1403  wefrc  5517  tz7.5  6184  f1ofveu  7134  fovrnda  7303  smoiso  7986  odi  8192  nndi  8236  nnmsucr  8238  f1oen2g  8513  f1dom2g  8514  domssex2  8665  ordunifi  8756  wemappo  9001  wemapso  9003  ackbij1lem16  9650  divneg  11325  divdiv32  11341  divneg2  11357  ltdiv2  11519  fimaxre  11577  fiminre  11580  suprzcl  12054  peano2uz  12293  infssuzle  12323  lbzbi  12328  zbtwnre  12338  irrmul  12365  supxrunb1  12704  expnlbnd  13594  hash1to3  13849  fun2dmnop  13853  brfi1uzind  13856  brcnvtrclfvcnv  14360  retancl  15490  tanneg  15496  demoivreALT  15549  dvdscmulr  15633  dvdsmulcr  15634  mulmoddvds  15674  gcd0id  15860  euclemma  16050  phiprmpw  16106  fermltl  16114  vdwapun  16303  vdwapid1  16304  cshwshashlem1  16424  fsets  16511  pospo  17578  latasymb  17659  mndcl  17914  imasmnd2  17943  gsumsgrpccat  17999  grpcl  18106  dfgrp2  18123  grprcan  18132  grpsubcl  18174  imasgrp2  18209  mhmid  18215  mhmmnd  18216  mulginvcom  18247  mulgnndir  18251  mulgnnass  18257  qusgrp  18330  ghmmulg  18365  ghmrn  18366  ghmeqker  18380  gsumccatsymgsn  18549  ablcom  18919  ablinvadd  18926  mulgmhm  18944  mulgghm  18945  ghmcmn  18948  odadd1  18964  odadd2  18965  srgcl  19258  srgacl  19270  srgcom  19271  ringcl  19310  crngcom  19311  ringacl  19327  imasring  19368  irredlmul  19457  rhmmul  19478  drngmcl  19511  isdrngd  19523  subrgacl  19542  subrgugrp  19550  srngadd  19624  srngmul  19625  idsrngd  19629  lmodacl  19641  lmodmcl  19642  lmodvacl  19644  lmodvsubcl  19675  lmod4  19680  lmodvaddsub4  19682  lmodvpncan  19683  lmodvnpcan  19684  lmodsubeq0  19689  pwssplit3  19829  islbs2  19922  islbs3  19923  lbsext  19931  rspssp  19995  zlmlmod  20219  psgnco  20275  ipdir  20331  ip2eq  20345  ocvin  20366  frlmsplit2  20465  ascldimul  20576  ascldimulOLD  20577  rnasclmulcl  20583  mplbas2  20713  coe1add  20896  coe1subfv  20898  coe1mul2  20901  ringvcl  21008  cramer  21299  chpmat1d  21444  filin  22462  filfinnfr  22485  filuni  22493  ufprim  22517  uffinfix  22535  hausflf  22605  uffcfflf  22647  cnextcn  22675  tmdmulg  22700  tsmsxplem1  22761  psmetcl  22917  xmetcl  22941  metcl  22942  meteq0  22949  metge0  22955  metsym  22960  metgt0  22969  blelrnps  23026  blelrn  23027  blssm  23028  blres  23041  mscl  23071  xmscl  23072  xmsge0  23073  xmseq0  23074  xmssym  23075  mopnin  23107  nmf2  23202  ngpdsr  23214  ngpds2  23215  ngpds2r  23216  ngpds3  23217  ngpds3r  23218  nmge0  23226  nmeq0  23227  nm2dif  23234  nmmul  23273  nlmmul0or  23292  nmods  23353  clmsub  23688  clmacl  23692  clmmcl  23693  clmsubcl  23694  clmvscl  23696  clmvsubval  23717  ncvsprp  23760  ncvsdif  23763  ncvspds  23769  cphnmvs  23798  cphipcl  23799  cphipcj  23807  cphorthcom  23809  cphipval2  23848  4cphipval2  23849  cphipval  23850  fmcfil  23879  mbfi1fseqlem3  24324  mbfi1fseqlem4  24325  mbfi1fseqlem5  24326  deg1ldgdomn  24698  drnguc1p  24774  quotval  24891  sincosq1sgn  25094  sincosq2sgn  25095  sincosq3sgn  25096  sincosq4sgn  25097  efabl  25145  lgsneg1  25909  dchrisumlem3  26078  ax5seglem2  26726  usgredg2vtx  27012  uspgredg2vtxeu  27013  usgredg2vtxeu  27014  cplgr3v  27228  vtxdumgr0nedg  27286  clwlkclwwlk  27790  frgrncvvdeqlem8  28094  grpocl  28286  grpodivcl  28325  ablomuldiv  28338  ablodivdiv4  28340  ablonnncan1  28343  vccl  28349  nvgcl  28406  nvcom  28407  nvadd4  28411  nvscl  28412  nvmval  28428  nvmcl  28432  nmcvcn  28481  nmlnoubi  28582  isblo3i  28587  blometi  28589  dipsubdir  28634  hlpar2  28682  hlpar  28683  hlcom  28686  hlipcj  28697  hlipgt0  28700  his52  28873  shintcli  29115  chlub  29295  homulass  29588  adjadj  29722  nmophmi  29817  kbass6  29907  atcvatlem  30171  mdsymlem3  30191  mdsymlem5  30193  rexdiv  30631  tltnle  30678  tlt3  30681  toslublem  30683  tosglblem  30685  archiabllem1b  30874  archiabllem2  30879  slmdacl  30890  slmdmcl  30891  slmdvacl  30893  qusscaval  30975  cringm4  31030  aean  31611  fiunelcarsg  31682  probcun  31784  probdif  31786  cndprobin  31800  f1resrcmplf1dlem  32467  cusgredgex  32476  swrdwlk  32481  satefvfmla1  32780  climuzcnv  33022  pibt2  34829  matunitlindflem1  35046  mblfinlem1  35087  mblfinlem2  35088  ftc1anclem6  35128  ssbnd  35219  heibor1  35241  exidcl  35307  rngocl  35332  rngogcl  35343  rngocom  35344  rngoa4  35347  rngosub  35361  rngonegmn1l  35372  rngonegmn1r  35373  ispridlc  35501  lshpcmp  36277  opltcon3b  36493  oldmm1  36506  olj01  36514  latm32  36520  omllaw4  36535  omllaw5N  36536  cmtcomlemN  36537  cmt2N  36539  cmtbr2N  36542  cmtbr3N  36543  cmtbr4N  36544  glbconxN  36667  hlexch1  36671  hlexch2  36672  hlexchb1  36673  hlexchb2  36674  hlexch3  36680  hlexch4N  36681  hlatexchb1  36682  hlatexchb2  36683  hlatexch1  36684  hlatexch2  36685  hlatle  36687  hlateq  36688  hlrelat1  36689  hlrelat2  36692  cvr1  36699  cvrval5  36704  cvrp  36705  atcvr1  36706  atcvr2  36707  cvrexchlem  36708  cvrexch  36709  dalem54  37015  pmaple  37050  pmap11  37051  paddass  37127  pmapj2N  37218  pmapocjN  37219  trlval2  37452  nnproddivdvdsd  39282  fsuppssind  39446  0prjspnlem  39599  grumnudlem  40980  eelT00  41398  eelTTT  41399  eelT11  41400  eelT12  41402  eelTT1  41403  eelT01  41404  mullimc  42245  mullimcf  42252  stoweidlem52  42681  stoweidlem60  42689  rngcl  44494  nzerooringczr  44683  ply1mulgsum  44785  itschlc0xyqsol1  45167  sinhpcosh  45253  reseccl  45266  recsccl  45267  recotcl  45268  onetansqsecsq  45274
  Copyright terms: Public domain W3C validator