Theorem syl3an1 1163

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  3adant1l  1177  3adant1r  1178  syl3an1b  1405  syl3an1br  1408  wefrc  5648  tz7.5  6373  f1cdmsn  7274  f1ofvswap  7298  f1ofveu  7397  fovcdmda  7576  suppvalfng  8164  smoiso  8374  odi  8589  nndi  8633  nnmsucr  8635  f1oen2g  8981  f1dom2g  8982  domssex2  9149  dif1ennn  9173  enfii  9198  phplem2  9217  php  9219  php3  9221  findcard3  9288  ordunifi  9296  nnsdomg  9305  ackbij1lem16  10246  divneg  11931  divdiv32  11947  divneg2  11963  ltdiv2  12126  fimaxre  12184  fiminre  12187  suprzcl  12671  peano2uz  12915  infssuzle  12945  lbzbi  12950  zbtwnre  12960  irrmul  12988  supxrunb1  13333  expnlbnd  14249  hash1to3  14508  fun2dmnop  14521  brfi1uzind  14524  brcnvtrclfvcnv  15022  retancl  16158  tanneg  16164  demoivreALT  16217  dvdscmulr  16302  dvdsmulcr  16303  mulmoddvds  16347  gcd0id  16536  euclemma  16730  phiprmpw  16793  fermltl  16801  vdwapun  16992  vdwapid1  16993  cshwshashlem1  17113  fsets  17186  pospo  18353  tltnle  18430  latasymb  18450  sgrpcl  18702  mndcl  18718  imasmnd2  18750  gsumsgrpccat  18816  grpcl  18922  dfgrp2  18943  grprcan  18954  grpsubcl  19001  imasgrp2  19036  mhmid  19044  mhmmnd  19045  mulginvcom  19080  mulgnndir  19084  mulgnnass  19090  qusgrp  19167  ghmmulg  19209  ghmrn  19210  ghmeqker  19224  gsumccatsymgsn  19405  ablcom  19778  ablinvadd  19786  mulgmhm  19806  mulgghm  19807  ghmcmn  19810  odadd1  19827  odadd2  19828  rngacl  20120  rngcl  20122  rngpropd  20132  srgcl  20151  srgacl  20163  srgcom  20164  ringcl  20208  crngcom  20209  ringacl  20236  pwspjmhmmgpd  20286  imasring  20288  irredlmul  20386  rhmmul  20444  subrngacl  20514  subrgacl  20541  subrgmcl  20542  subrgugrp  20549  isdomn4  20674  drngmclOLD  20709  isdrngd  20723  isdrngdOLD  20725  srngadd  20809  srngmul  20810  idsrngd  20814  lmodacl  20827  lmodmcl  20828  lmodvacl  20830  lmodvsubcl  20862  lmod4  20867  lmodvaddsub4  20869  lmodvpncan  20870  lmodvnpcan  20871  lmodsubeq0  20876  pwssplit3  21017  islbs2  21113  islbs3  21114  lbsext  21122  rspssp  21198  nzerooringczr  21439  zlmlmod  21481  psgnco  21541  ipdir  21597  ip2eq  21611  ocvin  21632  frlmsplit2  21731  ascldimul  21846  rnasclmulcl  21852  mplbas2  21998  coe1add  22199  coe1subfv  22201  coe1mul2  22204  rhmply1vsca  22324  ringvcl  22336  cramer  22627  chpmat1d  22772  filin  23790  filfinnfr  23813  filuni  23821  ufprim  23845  uffinfix  23863  hausflf  23933  uffcfflf  23975  cnextcn  24003  tmdmulg  24028  tsmsxplem1  24089  psmetcl  24244  xmetcl  24268  metcl  24269  meteq0  24276  metge0  24282  metsym  24287  metgt0  24296  blelrnps  24353  blelrn  24354  blssm  24355  blres  24368  mscl  24398  xmscl  24399  xmsge0  24400  xmseq0  24401  xmssym  24402  mopnin  24434  nmf2  24530  ngpdsr  24542  ngpds2  24543  ngpds2r  24544  ngpds3  24545  ngpds3r  24546  nmge0  24554  nmeq0  24555  nm2dif  24562  nmmul  24601  nlmmul0or  24620  nmods  24681  clmsub  25029  clmacl  25033  clmmcl  25034  clmsubcl  25035  clmvscl  25037  clmvsubval  25058  ncvsprp  25102  ncvsdif  25105  ncvspds  25111  cphnmvs  25140  cphipcl  25141  cphipcj  25149  cphorthcom  25151  cphipval2  25191  4cphipval2  25192  cphipval  25193  fmcfil  25222  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  deg1ldgdomn  26049  drnguc1p  26129  quotval  26250  sincosq1sgn  26457  sincosq2sgn  26458  sincosq3sgn  26459  sincosq4sgn  26460  efabl  26509  lgsneg1  27283  dchrisumlem3  27452  ax5seglem2  28854  usgredg2vtx  29144  uspgredg2vtxeu  29145  usgredg2vtxeu  29146  cplgr3v  29360  vtxdumgr0nedg  29419  clwlkclwwlk  29929  frgrncvvdeqlem8  30233  grpocl  30427  grpodivcl  30466  ablomuldiv  30479  ablodivdiv4  30481  ablonnncan1  30484  vccl  30490  nvgcl  30547  nvcom  30548  nvadd4  30552  nvscl  30553  nvmval  30569  nvmcl  30573  nmcvcn  30622  nmlnoubi  30723  isblo3i  30728  blometi  30730  dipsubdir  30775  hlpar2  30823  hlpar  30824  hlcom  30827  hlipcj  30838  hlipgt0  30841  his52  31014  shintcli  31256  chlub  31436  homulass  31729  adjadj  31863  nmophmi  31958  kbass6  32048  atcvatlem  32312  mdsymlem3  32332  mdsymlem5  32334  suppiniseg  32609  rexdiv  32846  tlt3  32896  toslublem  32898  tosglblem  32900  archiabllem1b  33136  archiabllem2  33141  slmdacl  33152  slmdmcl  33153  slmdvacl  33155  lidlincl  33391  cringm4  33407  evls1fldgencl  33657  aean  34221  fiunelcarsg  34294  probcun  34396  probdif  34398  cndprobin  34412  f1resrcmplf1dlem  35063  cusgredgex  35090  swrdwlk  35095  satefvfmla1  35393  climuzcnv  35639  pibt2  37381  matunitlindflem1  37586  mblfinlem1  37627  mblfinlem2  37628  ftc1anclem6  37668  ssbnd  37758  heibor1  37780  exidcl  37846  rngocl  37871  rngogcl  37882  rngocom  37883  rngoa4  37886  rngosub  37900  rngonegmn1l  37911  rngonegmn1r  37912  ispridlc  38040  lshpcmp  38952  opltcon3b  39168  oldmm1  39181  olj01  39189  latm32  39195  omllaw4  39210  omllaw5N  39211  cmtcomlemN  39212  cmt2N  39214  cmtbr2N  39217  cmtbr3N  39218  cmtbr4N  39219  glbconxN  39343  hlexch1  39347  hlexch2  39348  hlexchb1  39349  hlexchb2  39350  hlexch3  39356  hlexch4N  39357  hlatexchb1  39358  hlatexchb2  39359  hlatexch1  39360  hlatexch2  39361  hlatle  39363  hlateq  39364  hlrelat1  39365  hlrelat2  39368  cvr1  39375  cvrval5  39380  cvrp  39381  atcvr1  39382  atcvr2  39383  cvrexchlem  39384  cvrexch  39385  dalem54  39691  pmaple  39726  pmap11  39727  paddass  39803  pmapj2N  39894  pmapocjN  39895  trlval2  40128  nnproddivdvdsd  41959  fsuppssind  42563  mhphf  42567  0prjspnlem  42593  grumnudlem  44257  eelT00  44677  eelTTT  44678  eelT11  44679  eelT12  44681  eelTT1  44682  eelT01  44683  mullimc  45593  mullimcf  45600  dvmptfprod  45922  stoweidlem52  46029  stoweidlem60  46037  focofob  47057  f1ocof1ob  47058  clnbgrgrim  47895  ply1mulgsum  48314  itschlc0xyqsol1  48694  sinhpcosh  49552  reseccl  49565  recsccl  49566  recotcl  49567  onetansqsecsq  49573