Theorem syl3an1 1164

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

Step	Hyp	Ref	Expression
1		syl3an1.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	3anim1i 1153	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an1.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 17	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3adant1l  1178  3adant1r  1179  syl3an1b  1406  syl3an1br  1409  wefrc  5625  tz7.5  6344  f1cdmsn  7237  f1ofvswap  7261  f1ofveu  7361  fovcdmda  7538  suppvalfng  8117  smoiso  8302  odi  8514  nndi  8559  nnmsucr  8561  f1oen2g  8915  f1dom2g  8916  domssex2  9075  dif1ennn  9097  enfii  9120  phplem2  9139  php  9141  php3  9143  findcard3  9193  ordunifi  9200  nnsdomg  9209  ackbij1lem16  10156  divneg  11846  divdiv32  11863  divneg2  11879  ltdiv2  12042  fimaxre  12100  fiminre  12103  suprzcl  12609  peano2uz  12851  infssuzle  12881  lbzbi  12886  zbtwnre  12896  irrmul  12924  supxrunb1  13271  expnlbnd  14195  hash1to3  14454  fun2dmnop  14467  brfi1uzind  14470  brcnvtrclfvcnv  14967  retancl  16109  tanneg  16115  demoivreALT  16168  dvdscmulr  16253  dvdsmulcr  16254  mulmoddvds  16299  gcd0id  16488  euclemma  16683  phiprmpw  16746  fermltl  16754  vdwapun  16945  vdwapid1  16946  cshwshashlem1  17066  fsets  17139  pospo  18309  tltnle  18386  latasymb  18408  sgrpcl  18694  mndcl  18710  imasmnd2  18742  gsumsgrpccat  18808  grpcl  18917  dfgrp2  18938  grprcan  18949  grpsubcl  18996  imasgrp2  19031  mhmid  19039  mhmmnd  19040  mulginvcom  19075  mulgnndir  19079  mulgnnass  19085  qusgrp  19161  ghmmulg  19203  ghmrn  19204  ghmeqker  19218  gsumccatsymgsn  19401  ablcom  19774  ablinvadd  19782  mulgmhm  19802  mulgghm  19803  ghmcmn  19806  odadd1  19823  odadd2  19824  rngacl  20143  rngcl  20145  rngpropd  20155  srgcl  20174  srgacl  20186  srgcom  20187  ringcl  20231  crngcom  20232  ringacl  20259  pwspjmhmmgpd  20307  imasring  20310  irredlmul  20408  rhmmul  20465  subrngacl  20533  subrgacl  20560  subrgmcl  20561  subrgugrp  20568  isdomn4  20693  drngmclOLD  20728  isdrngd  20742  isdrngdOLD  20744  srngadd  20828  srngmul  20829  idsrngd  20833  lmodacl  20867  lmodmcl  20868  lmodvacl  20870  lmodvsubcl  20902  lmod4  20907  lmodvaddsub4  20909  lmodvpncan  20910  lmodvnpcan  20911  lmodsubeq0  20916  pwssplit3  21056  islbs2  21152  islbs3  21153  lbsext  21161  rspssp  21237  nzerooringczr  21460  zlmlmod  21502  psgnco  21563  ipdir  21619  ip2eq  21633  ocvin  21654  frlmsplit2  21753  ascldimul  21868  rnasclmulcl  21874  mplbas2  22020  coe1add  22229  coe1subfv  22231  coe1mul2  22234  rhmply1vsca  22353  ringvcl  22365  cramer  22656  chpmat1d  22801  filin  23819  filfinnfr  23842  filuni  23850  ufprim  23874  uffinfix  23892  hausflf  23962  uffcfflf  24004  cnextcn  24032  tmdmulg  24057  tsmsxplem1  24118  psmetcl  24272  xmetcl  24296  metcl  24297  meteq0  24304  metge0  24310  metsym  24315  metgt0  24324  blelrnps  24381  blelrn  24382  blssm  24383  blres  24396  mscl  24426  xmscl  24427  xmsge0  24428  xmseq0  24429  xmssym  24430  mopnin  24462  nmf2  24558  ngpdsr  24570  ngpds2  24571  ngpds2r  24572  ngpds3  24573  ngpds3r  24574  nmge0  24582  nmeq0  24583  nm2dif  24590  nmmul  24629  nlmmul0or  24648  nmods  24709  clmsub  25047  clmacl  25051  clmmcl  25052  clmsubcl  25053  clmvscl  25055  clmvsubval  25076  ncvsprp  25119  ncvsdif  25122  ncvspds  25128  cphnmvs  25157  cphipcl  25158  cphipcj  25166  cphorthcom  25168  cphipval2  25208  4cphipval2  25209  cphipval  25210  fmcfil  25239  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  deg1ldgdomn  26059  drnguc1p  26139  quotval  26258  sincosq1sgn  26462  sincosq2sgn  26463  sincosq3sgn  26464  sincosq4sgn  26465  efabl  26514  lgsneg1  27285  dchrisumlem3  27454  bdayn0p1  28361  ax5seglem2  28998  usgredg2vtx  29288  uspgredg2vtxeu  29289  usgredg2vtxeu  29290  cplgr3v  29504  vtxdumgr0nedg  29562  clwlkclwwlk  30072  frgrncvvdeqlem8  30376  grpocl  30571  grpodivcl  30610  ablomuldiv  30623  ablodivdiv4  30625  ablonnncan1  30628  vccl  30634  nvgcl  30691  nvcom  30692  nvadd4  30696  nvscl  30697  nvmval  30713  nvmcl  30717  nmcvcn  30766  nmlnoubi  30867  isblo3i  30872  blometi  30874  dipsubdir  30919  hlpar2  30967  hlpar  30968  hlcom  30971  hlipcj  30982  hlipgt0  30985  his52  31158  shintcli  31400  chlub  31580  homulass  31873  adjadj  32007  nmophmi  32102  kbass6  32192  atcvatlem  32456  mdsymlem3  32476  mdsymlem5  32478  suppiniseg  32759  rexdiv  32985  tlt3  33030  toslublem  33032  tosglblem  33034  archiabllem1b  33253  archiabllem2  33258  slmdacl  33270  slmdmcl  33271  slmdvacl  33273  lidlincl  33490  cringm4  33506  evls1fldgencl  33814  aean  34388  fiunelcarsg  34460  probcun  34562  probdif  34564  cndprobin  34578  f1resrcmplf1dlem  35229  rankfilimbi  35244  cusgredgex  35304  swrdwlk  35309  satefvfmla1  35607  climuzcnv  35853  pibt2  37733  matunitlindflem1  37937  mblfinlem1  37978  mblfinlem2  37979  ftc1anclem6  38019  ssbnd  38109  heibor1  38131  exidcl  38197  rngocl  38222  rngogcl  38233  rngocom  38234  rngoa4  38237  rngosub  38251  rngonegmn1l  38262  rngonegmn1r  38263  ispridlc  38391  lshpcmp  39434  opltcon3b  39650  oldmm1  39663  olj01  39671  latm32  39677  omllaw4  39692  omllaw5N  39693  cmtcomlemN  39694  cmt2N  39696  cmtbr2N  39699  cmtbr3N  39700  cmtbr4N  39701  glbconxN  39824  hlexch1  39828  hlexch2  39829  hlexchb1  39830  hlexchb2  39831  hlexch3  39837  hlexch4N  39838  hlatexchb1  39839  hlatexchb2  39840  hlatexch1  39841  hlatexch2  39842  hlatle  39844  hlateq  39845  hlrelat1  39846  hlrelat2  39849  cvr1  39856  cvrval5  39861  cvrp  39862  atcvr1  39863  atcvr2  39864  cvrexchlem  39865  cvrexch  39866  dalem54  40172  pmaple  40207  pmap11  40208  paddass  40284  pmapj2N  40375  pmapocjN  40376  trlval2  40609  nnproddivdvdsd  42439  fsuppssind  43026  mhphf  43030  0prjspnlem  43056  grumnudlem  44712  eelT00  45131  eelTTT  45132  eelT11  45133  eelT12  45135  eelTT1  45136  eelT01  45137  mullimc  46046  mullimcf  46053  dvmptfprod  46373  stoweidlem52  46480  stoweidlem60  46488  focofob  47528  f1ocof1ob  47529  clnbgrgrim  48410  ply1mulgsum  48866  itschlc0xyqsol1  49242  sinhpcosh  50215  reseccl  50228  recsccl  50229  recotcl  50230  onetansqsecsq  50236