Theorem syl3an1 1175

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3adant1l  1189  3adant1r  1190  syl3an1b  1421  syl3an1br  1424  wefrc  5637  tz7.5  6362  f1cdmsn  7261  f1ofvswap  7285  f1ofveu  7385  fovcdmda  7562  suppvalfng  8141  smoiso  8327  odi  8542  nndi  8587  nnmsucr  8589  f1oen2g  8943  f1dom2g  8944  domssex2  9103  dif1ennn  9125  enfii  9148  phplem2  9167  php  9169  php3  9171  findcard3  9221  ordunifi  9228  nnsdomg  9237  ackbij1lem16  10184  divneg  11876  divdiv32  11893  divneg2  11909  ltdiv2  12072  fimaxre  12130  fiminre  12133  suprzcl  12647  peano2uz  12896  infssuzle  12926  lbzbi  12931  zbtwnre  12941  irrmul  12969  supxrunb1  13316  expnlbnd  14240  hash1to3  14499  fun2dmnop  14512  brfi1uzind  14515  brcnvtrclfvcnv  15012  retancl  16165  tanneg  16171  demoivreALT  16224  dvdscmulr  16309  dvdsmulcr  16310  mulmoddvds  16355  gcd0id  16544  euclemma  16739  phiprmpw  16802  fermltl  16810  vdwapun  17001  vdwapid1  17002  cshwshashlem1  17122  fsets  17196  pospo  18366  tltnle  18443  latasymb  18465  sgrpcl  18751  mndcl  18767  imasmnd2  18799  gsumsgrpccat  18865  grpcl  18974  dfgrp2  18995  grprcan  19006  grpsubcl  19053  imasgrp2  19088  mhmid  19096  mhmmnd  19097  mulginvcom  19132  mulgnndir  19136  mulgnnass  19142  qusgrp  19218  ghmmulg  19259  ghmrn  19260  ghmeqker  19274  gsumccatsymgsn  19457  ablcom  19830  ablinvadd  19838  mulgmhm  19858  mulgghm  19859  ghmcmn  19862  odadd1  19879  odadd2  19880  rngacl  20199  rngcl  20201  rngpropd  20211  srgcl  20230  srgacl  20242  srgcom  20243  ringcl  20287  crngcom  20288  ringacl  20315  pwspjmhmmgpd  20363  imasring  20366  irredlmul  20464  rhmmul  20522  subrngacl  20593  subrgacl  20620  subrgmcl  20621  subrgugrp  20628  isdomn4  20753  drngmclOLD  20788  isdrngd  20802  isdrngdOLD  20804  srngadd  20888  srngmul  20889  idsrngd  20893  lmodacl  20927  lmodmcl  20928  lmodvacl  20930  lmodvsubcl  20962  lmod4  20967  lmodvaddsub4  20969  lmodvpncan  20970  lmodvnpcan  20971  lmodsubeq0  20976  pwssplit3  21116  islbs2  21212  islbs3  21213  lbsext  21221  rspssp  21297  nzerooringczr  21520  zlmlmod  21562  psgnco  21623  ipdir  21679  ip2eq  21693  ocvin  21714  frlmsplit2  21813  ascldimul  21928  rnasclmulcl  21934  mplbas2  22083  coe1add  22315  coe1subfv  22317  coe1mul2  22320  rhmply1vsca  22436  ringvcl  22448  cramer  22739  chpmat1d  22884  filin  23902  filfinnfr  23925  filuni  23933  ufprim  23957  uffinfix  23975  hausflf  24045  uffcfflf  24087  cnextcn  24115  tmdmulg  24140  tsmsxplem1  24201  psmetcl  24355  xmetcl  24379  metcl  24380  meteq0  24387  metge0  24393  metsym  24398  metgt0  24407  blelrnps  24464  blelrn  24465  blssm  24466  blres  24479  mscl  24509  xmscl  24510  xmsge0  24511  xmseq0  24512  xmssym  24513  mopnin  24545  nmf2  24641  ngpdsr  24653  ngpds2  24654  ngpds2r  24655  ngpds3  24656  ngpds3r  24657  nmge0  24665  nmeq0  24666  nm2dif  24673  nmmul  24712  nlmmul0or  24731  nmods  24792  clmsub  25130  clmacl  25134  clmmcl  25135  clmsubcl  25136  clmvscl  25138  clmvsubval  25159  ncvsprp  25202  ncvsdif  25205  ncvspds  25211  cphnmvs  25240  cphipcl  25241  cphipcj  25249  cphorthcom  25251  cphipval2  25291  4cphipval2  25292  cphipval  25293  fmcfil  25322  mbfi1fseqlem3  25767  mbfi1fseqlem4  25768  mbfi1fseqlem5  25769  deg1ldgdomn  26142  drnguc1p  26222  quotval  26344  sincosq1sgn  26551  sincosq2sgn  26552  sincosq3sgn  26553  sincosq4sgn  26554  efabl  26603  lgsneg1  27374  dchrisumlem3  27543  bdayn0p1  28450  ax5seglem2  29087  usgredg2vtx  29377  uspgredg2vtxeu  29378  usgredg2vtxeu  29379  cplgr3v  29593  vtxdumgr0nedg  29651  clwlkclwwlk  30161  frgrncvvdeqlem8  30465  grpocl  30660  grpodivcl  30699  ablomuldiv  30712  ablodivdiv4  30714  ablonnncan1  30717  vccl  30723  nvgcl  30780  nvcom  30781  nvadd4  30785  nvscl  30786  nvmval  30802  nvmcl  30806  nmcvcn  30855  nmlnoubi  30956  isblo3i  30961  blometi  30963  dipsubdir  31008  hlpar2  31056  hlpar  31057  hlcom  31060  hlipcj  31071  hlipgt0  31074  his52  31247  shintcli  31489  chlub  31669  homulass  31962  adjadj  32096  nmophmi  32191  kbass6  32281  atcvatlem  32545  mdsymlem3  32565  mdsymlem5  32567  suppiniseg  32849  rexdiv  33064  tlt3  33109  toslublem  33111  tosglblem  33113  archiabllem1b  33333  archiabllem2  33338  slmdacl  33350  slmdmcl  33351  slmdvacl  33353  lidlincl  33577  cringm4  33593  evls1fldgencl  33928  aean  34502  fiunelcarsg  34574  probcun  34676  probdif  34678  cndprobin  34692  f1resrcmplf1dlem  35341  rankfilimbi  35358  cusgredgex  35433  swrdwlk  35438  satefvfmla1  35736  climuzcnv  35982  pibt2  37872  matunitlindflem1  38076  mblfinlem1  38117  mblfinlem2  38118  ftc1anclem6  38158  ssbnd  38248  heibor1  38270  exidcl  38336  rngocl  38361  rngogcl  38372  rngocom  38373  rngoa4  38376  rngosub  38390  rngonegmn1l  38401  rngonegmn1r  38402  ispridlc  38530  lshpcmp  39573  opltcon3b  39789  oldmm1  39802  olj01  39810  latm32  39816  omllaw4  39831  omllaw5N  39832  cmtcomlemN  39833  cmt2N  39835  cmtbr2N  39838  cmtbr3N  39839  cmtbr4N  39840  glbconxN  39963  hlexch1  39967  hlexch2  39968  hlexchb1  39969  hlexchb2  39970  hlexch3  39976  hlexch4N  39977  hlatexchb1  39978  hlatexchb2  39979  hlatexch1  39980  hlatexch2  39981  hlatle  39983  hlateq  39984  hlrelat1  39985  hlrelat2  39988  cvr1  39995  cvrval5  40000  cvrp  40001  atcvr1  40002  atcvr2  40003  cvrexchlem  40004  cvrexch  40005  dalem54  40311  pmaple  40346  pmap11  40347  paddass  40423  pmapj2N  40514  pmapocjN  40515  trlval2  40748  nnproddivdvdsd  42578  fsuppssind  43136  mhphf  43140  0prjspnlem  43166  grumnudlem  44822  eelT00  45241  eelTTT  45242  eelT11  45243  eelT12  45245  eelTT1  45246  eelT01  45247  mullimc  46153  mullimcf  46160  dvmptfprod  46480  stoweidlem52  46587  stoweidlem60  46595  focofob  47635  f1ocof1ob  47636  clnbgrgrim  48517  ply1mulgsum  48973  itschlc0xyqsol1  49349  sinhpcosh  50322  reseccl  50335  recsccl  50336  recotcl  50337  onetansqsecsq  50343