Theorem syl3an1 1159

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3adant1l  1172  3adant1r  1173  syl3an1b  1399  syl3an1br  1402  wefrc  5549  tz7.5  6212  f1ofveu  7151  fovrnda  7319  smoiso  7999  odi  8205  nndi  8249  nnmsucr  8251  f1oen2g  8526  f1dom2g  8527  domssex2  8677  ordunifi  8768  wemappo  9013  wemapso  9015  ackbij1lem16  9657  divneg  11332  divdiv32  11348  divneg2  11364  ltdiv2  11526  fimaxre  11584  fimaxreOLD  11585  fiminre  11588  suprzcl  12063  peano2uz  12302  infssuzle  12332  lbzbi  12337  zbtwnre  12347  irrmul  12374  supxrunb1  12713  expnlbnd  13595  hash1to3  13850  fun2dmnop  13854  brfi1uzind  13857  brcnvtrclfvcnv  14365  retancl  15495  tanneg  15501  demoivreALT  15554  dvdscmulr  15638  dvdsmulcr  15639  mulmoddvds  15679  gcd0id  15867  euclemma  16057  phiprmpw  16113  fermltl  16121  vdwapun  16310  vdwapid1  16311  cshwshashlem1  16429  fsets  16516  pospo  17583  latasymb  17664  mndcl  17919  imasmnd2  17948  gsumsgrpccat  18004  grpcl  18111  dfgrp2  18128  grprcan  18137  grpsubcl  18179  imasgrp2  18214  mhmid  18220  mhmmnd  18221  mulginvcom  18252  mulgnndir  18256  mulgnnass  18262  qusgrp  18335  ghmmulg  18370  ghmrn  18371  ghmeqker  18385  gsumccatsymgsn  18554  ablcom  18924  ablinvadd  18930  mulgmhm  18948  mulgghm  18949  ghmcmn  18952  odadd1  18968  odadd2  18969  srgcl  19262  srgacl  19274  srgcom  19275  ringcl  19311  crngcom  19312  ringacl  19328  imasring  19369  irredlmul  19458  rhmmul  19479  drngmcl  19515  isdrngd  19527  subrgacl  19546  subrgugrp  19554  srngadd  19628  srngmul  19629  idsrngd  19633  lmodacl  19645  lmodmcl  19646  lmodvacl  19648  lmodvsubcl  19679  lmod4  19684  lmodvaddsub4  19686  lmodvpncan  19687  lmodvnpcan  19688  lmodsubeq0  19693  pwssplit3  19833  islbs2  19926  islbs3  19927  lbsext  19935  rspssp  19999  ascldimul  20116  ascldimulOLD  20117  rnasclmulcl  20123  mplbas2  20251  coe1add  20432  coe1subfv  20434  coe1mul2  20437  zlmlmod  20670  psgnco  20727  ipdir  20783  ip2eq  20797  ocvin  20818  frlmsplit2  20917  ringvcl  21009  cramer  21300  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  23684  clmacl  23688  clmmcl  23689  clmsubcl  23690  clmvscl  23692  clmvsubval  23713  ncvsprp  23756  ncvsdif  23759  ncvspds  23765  cphnmvs  23794  cphipcl  23795  cphipcj  23803  cphorthcom  23805  cphipval2  23844  4cphipval2  23845  cphipval  23846  fmcfil  23875  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  deg1ldgdomn  24688  drnguc1p  24764  quotval  24881  sincosq1sgn  25084  sincosq2sgn  25085  sincosq3sgn  25086  sincosq4sgn  25087  efabl  25134  lgsneg1  25898  dchrisumlem3  26067  ax5seglem2  26715  usgredg2vtx  27001  uspgredg2vtxeu  27002  usgredg2vtxeu  27003  cplgr3v  27217  vtxdumgr0nedg  27275  clwlkclwwlk  27780  frgrncvvdeqlem8  28085  grpocl  28277  grpodivcl  28316  ablomuldiv  28329  ablodivdiv4  28331  ablonnncan1  28334  vccl  28340  nvgcl  28397  nvcom  28398  nvadd4  28402  nvscl  28403  nvmval  28419  nvmcl  28423  nmcvcn  28472  nmlnoubi  28573  isblo3i  28578  blometi  28580  dipsubdir  28625  hlpar2  28673  hlpar  28674  hlcom  28677  hlipcj  28688  hlipgt0  28691  his52  28864  shintcli  29106  chlub  29286  homulass  29579  adjadj  29713  nmophmi  29808  kbass6  29898  atcvatlem  30162  mdsymlem3  30182  mdsymlem5  30184  rexdiv  30602  tltnle  30649  tlt3  30652  toslublem  30654  tosglblem  30656  archiabllem1b  30821  archiabllem2  30826  slmdacl  30837  slmdmcl  30838  slmdvacl  30840  qusscaval  30921  cringm4  30962  aean  31503  fiunelcarsg  31574  probcun  31676  probdif  31678  cndprobin  31692  f1resrcmplf1dlem  32359  cusgredgex  32368  swrdwlk  32373  satefvfmla1  32672  climuzcnv  32914  pibt2  34701  matunitlindflem1  34903  mblfinlem1  34944  mblfinlem2  34945  ftc1anclem6  34987  ssbnd  35081  heibor1  35103  exidcl  35169  rngocl  35194  rngogcl  35205  rngocom  35206  rngoa4  35209  rngosub  35223  rngonegmn1l  35234  rngonegmn1r  35235  ispridlc  35363  lshpcmp  36139  opltcon3b  36355  oldmm1  36368  olj01  36376  latm32  36382  omllaw4  36397  omllaw5N  36398  cmtcomlemN  36399  cmt2N  36401  cmtbr2N  36404  cmtbr3N  36405  cmtbr4N  36406  glbconxN  36529  hlexch1  36533  hlexch2  36534  hlexchb1  36535  hlexchb2  36536  hlexch3  36542  hlexch4N  36543  hlatexchb1  36544  hlatexchb2  36545  hlatexch1  36546  hlatexch2  36547  hlatle  36549  hlateq  36550  hlrelat1  36551  hlrelat2  36554  cvr1  36561  cvrval5  36566  cvrp  36567  atcvr1  36568  atcvr2  36569  cvrexchlem  36570  cvrexch  36571  dalem54  36877  pmaple  36912  pmap11  36913  paddass  36989  pmapj2N  37080  pmapocjN  37081  trlval2  37314  0prjspnlem  39288  grumnudlem  40641  eelT00  41059  eelTTT  41060  eelT11  41061  eelT12  41063  eelTT1  41064  eelT01  41065  mullimc  41917  mullimcf  41924  stoweidlem52  42357  stoweidlem60  42365  rngcl  44174  nzerooringczr  44363  ply1mulgsum  44464  itschlc0xyqsol1  44773  sinhpcosh  44859  reseccl  44872  recsccl  44873  recotcl  44874  onetansqsecsq  44880