Theorem syl3an1 1179

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 1168	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an1.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 18	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  3adant1l  1193  3adant1r  1194  syl3an1b  1428  syl3an1br  1431  wefrc  5653  tz7.5  6379  f1cdmsn  7278  f1ofvswap  7302  f1ofveu  7402  fovcdmda  7579  suppvalfng  8159  smoiso  8345  odi  8560  nndi  8605  nnmsucr  8607  f1oen2g  8961  f1dom2g  8962  domssex2  9121  dif1ennn  9143  enfii  9166  phplem2  9185  php  9187  php3  9189  findcard3  9239  ordunifi  9246  nnsdomg  9255  ackbij1lem16  10213  divneg  11902  divdiv32  11919  divneg2  11935  ltdiv2  12097  fimaxre  12155  fiminre  12158  suprzcl  12672  peano2uz  12921  infssuzle  12951  lbzbi  12956  zbtwnre  12966  irrmul  12994  supxrunb1  13341  expnlbnd  14265  hash1to3  14525  fun2dmnop  14538  brfi1uzind  14541  brcnvtrclfvcnv  15038  retancl  16194  tanneg  16200  demoivreALT  16253  dvdscmulr  16338  dvdsmulcr  16339  mulmoddvds  16384  gcd0id  16573  euclemma  16768  phiprmpw  16831  fermltl  16839  vdwapun  17030  vdwapid1  17031  cshwshashlem1  17151  fsets  17225  pospo  18395  tltnle  18472  latasymb  18494  sgrpcl  18780  mndcl  18796  imasmnd2  18828  gsumsgrpccat  18895  grpcl  19004  dfgrp2  19025  grprcan  19036  grpsubcl  19082  imasgrp2  19117  mhmid  19125  mhmmnd  19126  mulginvcom  19161  mulgnndir  19165  mulgnnass  19171  qusgrp  19253  ghmmulg  19294  ghmrn  19295  ghmeqker  19309  gsumccatsymgsn  19492  ablcom  19865  ablinvadd  19873  mulgmhm  19893  mulgghm  19894  ghmcmn  19897  odadd1  19914  odadd2  19915  rngacl  20236  rngcl  20238  rngpropd  20248  srgcl  20271  srgacl  20283  srgcom  20284  ringcl  20328  crngcom  20329  ringacl  20357  pwspjmhmmgpd  20405  imasring  20408  irredlmul  20506  rhmmul  20564  subrngacl  20637  subrgacl  20664  subrgmcl  20665  subrgugrp  20672  isdomn4  20796  isdrngd  20843  isdrngdOLD  20845  ringen1zr0  20855  srngadd  20928  srngmul  20929  idsrngd  20933  lmodacl  20967  lmodmcl  20968  lmodvacl  20970  lmodvsubcl  21002  lmod4  21007  lmodvaddsub4  21009  lmodvpncan  21010  lmodvnpcan  21011  lmodsubeq0  21016  pwssplit3  21156  islbs2  21252  islbs3  21253  lbsext  21261  rspssp  21342  cringm4  21438  nzerooringczr  21595  zlmlmod  21637  psgnco  21698  ipdir  21754  ip2eq  21768  ocvin  21789  frlmsplit2  21888  ascldimul  22003  rnasclmulcl  22009  mplbas2  22158  coe1add  22390  coe1subfv  22392  coe1mul2  22395  rhmply1vsca  22510  ringvcl  22522  cramer  22813  chpmat1d  22958  filin  23976  filfinnfr  23999  filuni  24007  ufprim  24031  uffinfix  24049  hausflf  24119  uffcfflf  24161  cnextcn  24189  tmdmulg  24214  tsmsxplem1  24275  psmetcl  24429  xmetcl  24453  metcl  24454  meteq0  24461  metge0  24467  metsym  24472  metgt0  24481  blelrnps  24538  blelrn  24539  blssm  24540  blres  24553  mscl  24583  xmscl  24584  xmsge0  24585  xmseq0  24586  xmssym  24587  mopnin  24619  nmf2  24715  ngpdsr  24727  ngpds2  24728  ngpds2r  24729  ngpds3  24730  ngpds3r  24731  nmge0  24739  nmeq0  24740  nm2dif  24747  nmmul  24786  nlmmul0or  24805  nmods  24866  clmsub  25204  clmacl  25208  clmmcl  25209  clmsubcl  25210  clmvscl  25212  clmvsubval  25233  ncvsprp  25276  ncvsdif  25279  ncvspds  25285  cphnmvs  25314  cphipcl  25315  cphipcj  25323  cphorthcom  25325  cphipval2  25365  4cphipval2  25366  cphipval  25367  fmcfil  25396  mbfi1fseqlem3  25841  mbfi1fseqlem4  25842  mbfi1fseqlem5  25843  deg1ldgdomn  26216  drnguc1p  26296  quotval  26418  sincosq1sgn  26625  sincosq2sgn  26626  sincosq3sgn  26627  sincosq4sgn  26628  efabl  26677  lgsneg1  27448  dchrisumlem3  27617  bdayn0p1  28524  ax5seglem2  29216  usgredg2vtx  29506  uspgredg2vtxeu  29507  usgredg2vtxeu  29508  cplgr3v  29722  vtxdumgr0nedg  29780  clwlkclwwlk  30290  frgrncvvdeqlem8  30594  grpocl  30789  grpodivcl  30828  ablomuldiv  30841  ablodivdiv4  30843  ablonnncan1  30846  vccl  30852  nvgcl  30909  nvcom  30910  nvadd4  30914  nvscl  30915  nvmval  30931  nvmcl  30935  nmcvcn  30984  nmlnoubi  31085  isblo3i  31090  blometi  31092  dipsubdir  31137  hlpar2  31185  hlpar  31186  hlcom  31189  hlipcj  31200  hlipgt0  31203  his52  31376  shintcli  31618  chlub  31798  homulass  32091  adjadj  32225  nmophmi  32320  kbass6  32410  atcvatlem  32674  mdsymlem3  32694  mdsymlem5  32696  suppiniseg  32968  rexdiv  33182  tlt3  33227  toslublem  33229  tosglblem  33231  archiabllem1b  33449  archiabllem2  33454  slmdacl  33466  slmdmcl  33467  slmdvacl  33469  lidlincl  33678  evls1fldgencl  34001  aean  34575  fiunelcarsg  34647  probcun  34749  probdif  34751  cndprobin  34765  f1resrcmplf1dlem  35414  rankfilimbi  35433  cusgredgex  35509  swrdwlk  35514  satefvfmla1  35812  climuzcnv  36058  pibt2  37946  matunitlindflem1  38150  mblfinlem1  38191  mblfinlem2  38192  ftc1anclem6  38232  ssbnd  38322  heibor1  38344  exidcl  38410  rngocl  38435  rngogcl  38446  rngocom  38447  rngoa4  38450  rngosub  38464  rngonegmn1l  38475  rngonegmn1r  38476  ispridlc  38604  lshpcmp  39647  opltcon3b  39863  oldmm1  39876  olj01  39884  latm32  39890  omllaw4  39905  omllaw5N  39906  cmtcomlemN  39907  cmt2N  39909  cmtbr2N  39912  cmtbr3N  39913  cmtbr4N  39914  glbconxN  40037  hlexch1  40041  hlexch2  40042  hlexchb1  40043  hlexchb2  40044  hlexch3  40050  hlexch4N  40051  hlatexchb1  40052  hlatexchb2  40053  hlatexch1  40054  hlatexch2  40055  hlatle  40057  hlateq  40058  hlrelat1  40059  hlrelat2  40062  cvr1  40069  cvrval5  40074  cvrp  40075  atcvr1  40076  atcvr2  40077  cvrexchlem  40078  cvrexch  40079  dalem54  40385  pmaple  40420  pmap11  40421  paddass  40497  pmapj2N  40588  pmapocjN  40589  trlval2  40822  nnproddivdvdsd  42652  fsuppssind  43212  mhphf  43216  0prjspnlem  43242  grumnudlem  44882  eelT00  45300  eelTTT  45301  eelT11  45302  eelT12  45304  eelTT1  45305  eelT01  45306  mullimc  46219  mullimcf  46226  dvmptfprod  46546  stoweidlem52  46653  stoweidlem60  46661  focofob  47701  f1ocof1ob  47702  clnbgrgrim  48583  ply1mulgsum  49050  itschlc0xyqsol1  49426  sinhpcosh  50398  reseccl  50411  recsccl  50412  recotcl  50413  onetansqsecsq  50419