Theorem syl3an1 1351

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  syl3an1b  1354  syl3an1br  1357  wefrc  5032  tz7.5  5661  f1ofveu  6544  fovrnda  6703  smoiso  7346  odi  7546  nndi  7590  nnmsucr  7592  f1oen2g  7858  f1dom2g  7859  domssex2  8005  ordunifi  8095  wemappo  8337  wemapso  8339  ackbij1lem16  8940  divneg  10598  divdiv32  10612  divneg2  10628  ltdiv2  10788  fimaxre  10847  suprzcl  11333  peano2uz  11617  infssuzle  11647  lbzbi  11652  zbtwnre  11662  irrmul  11689  supxrunb1  12021  expnlbnd  12856  hash1to3  13128  fun2dmnop  13132  brfi1uzind  13135  brfi1uzindOLD  13141  brcnvtrclfvcnv  13594  retancl  14711  tanneg  14717  demoivreALT  14770  dvdscmulr  14848  dvdsmulcr  14849  gcd0id  15078  euclemma  15263  phiprmpw  15319  fermltl  15327  vdwapun  15516  vdwapid1  15517  cshwshashlem1  15640  fsets  15723  pospo  16796  latasymb  16877  mndcl  17124  imasmnd2  17150  grpcl  17253  dfgrp2  17270  grprcan  17278  grpsubcl  17318  imasgrp2  17353  mhmid  17359  mhmmnd  17360  mulginvcom  17388  qusgrp  17472  ghmmulg  17495  ghmrn  17496  ghmeqker  17510  gsumccatsymgsn  17669  ablcom  18033  ablinvadd  18038  mulgmhm  18056  mulgghm  18057  ghmcmn  18060  odadd1  18074  odadd2  18075  srgcl  18335  srgacl  18347  srgcom  18348  ringcl  18384  crngcom  18385  ringacl  18401  imasring  18442  irredlmul  18531  rhmmul  18550  drngmcl  18583  isdrngd  18595  subrgacl  18614  subrgugrp  18622  srngadd  18680  srngmul  18681  idsrngd  18685  lmodacl  18697  lmodmcl  18698  lmodvacl  18700  lmodvsubcl  18731  lmod4  18736  lmodvaddsub4  18738  lmodvpncan  18739  lmodvnpcan  18740  lmodsubeq0  18745  pwssplit3  18882  islbs2  18975  islbs3  18976  lbsext  18984  rspssp  19047  mplbas2  19291  coe1add  19455  coe1subfv  19457  coe1mul2  19460  zlmlmod  19690  psgnco  19748  ipdir  19803  ip2eq  19817  ocvin  19837  frlmsplit2  19931  ringvcl  20023  cramer  20316  chpmat1d  20460  filin  21468  filfinnfr  21491  filuni  21499  ufprim  21523  uffinfix  21541  hausflf  21611  uffcfflf  21653  cnextcn  21681  tmdmulg  21706  tsmsxplem1  21766  psmetcl  21922  xmetcl  21946  metcl  21947  meteq0  21954  metge0  21960  metsym  21965  metgt0  21974  blelrnps  22031  blelrn  22032  blssm  22033  blres  22046  mscl  22076  xmscl  22077  xmsge0  22078  xmseq0  22079  xmssym  22080  mopnin  22112  nmf2  22207  ngpdsr  22219  ngpds2  22220  ngpds2r  22221  ngpds3  22222  ngpds3r  22223  nmge0  22231  nmeq0  22232  nm2dif  22239  nmmul  22278  nlmmul0or  22297  nmods  22358  clmsub  22688  clmacl  22692  clmmcl  22693  clmsubcl  22694  clmvscl  22696  clmvsubval  22717  ncvsprp  22760  ncvsdif  22763  ncvspds  22769  cphnmvs  22798  cphipcl  22799  cphipcj  22807  cphorthcom  22809  cphipval2  22848  4cphipval2  22849  cphipval  22850  fmcfil  22878  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  deg1ldgdomn  23658  drnguc1p  23734  quotval  23851  sincosq1sgn  24054  sincosq2sgn  24055  sincosq3sgn  24056  sincosq4sgn  24057  efabl  24100  lgsneg1  24847  dchrisumlem3  24980  ax5seglem2  25609  wlkdvspthlem  26137  frg2spot1  26585  frgregordn0  26597  grpocl  26738  grpodivcl  26777  ablomuldiv  26790  ablodivdiv4  26792  ablonnncan  26794  ablonnncan1  26796  vccl  26802  nvgcl  26859  nvcom  26860  nvadd4  26864  nvscl  26865  nvmval  26881  nvmcl  26885  nmcvcn  26934  nmlnoubi  27035  isblo3i  27040  blometi  27042  dipsubdir  27087  hlpar2  27136  hlpar  27137  hlcom  27140  hlipcj  27151  hlipgt0  27154  his52  27328  shintcli  27572  chlub  27752  homulass  28045  adjadj  28179  nmophmi  28274  kbass6  28364  atcvatlem  28628  mdsymlem3  28648  mdsymlem5  28650  rexdiv  28965  tltnle  28993  tlt3  28996  toslublem  28998  tosglblem  29000  archiabllem1b  29077  archiabllem2  29082  slmdacl  29093  slmdmcl  29094  slmdvacl  29096  aean  29634  fiunelcarsg  29705  probcun  29807  probdif  29809  cndprobin  29823  climuzcnv  30819  matunitlindflem1  32575  mblfinlem1  32616  mblfinlem2  32617  ftc1anclem6  32660  ssbnd  32757  heibor1  32779  exidcl  32845  rngocl  32870  rngogcl  32881  rngocom  32882  rngoa4  32885  rngosub  32899  rngonegmn1l  32910  rngonegmn1r  32911  ispridlc  33039  lshpcmp  33293  opltcon3b  33509  oldmm1  33522  olj01  33530  latm32  33536  omllaw4  33551  omllaw5N  33552  cmtcomlemN  33553  cmt2N  33555  cmtbr2N  33558  cmtbr3N  33559  cmtbr4N  33560  glbconxN  33682  hlexch1  33686  hlexch2  33687  hlexchb1  33688  hlexchb2  33689  hlexch3  33695  hlexch4N  33696  hlatexchb1  33697  hlatexchb2  33698  hlatexch1  33699  hlatexch2  33700  hlatle  33702  hlateq  33703  hlrelat1  33704  hlrelat2  33707  cvr1  33714  cvrval5  33719  cvrp  33720  atcvr1  33721  atcvr2  33722  cvrexchlem  33723  cvrexch  33724  dalem54  34030  pmaple  34065  pmap11  34066  paddass  34142  pmapj2N  34233  pmapocjN  34234  trlval2  34468  eelT00  37951  eelTTT  37952  eelT11  37953  eelT12  37955  eelTT1  37956  eelT01  37957  mullimc  38683  mullimcf  38690  stoweidlem52  38945  stoweidlem60  38953  usgredg2vtx  40446  uspgredg2vtxeu  40447  usgredg2vtxeu  40448  cplgr3v  40657  vtxdumgr0nedg  40708  wlkwwlkinj  41093  wlkwwlksur  41094  clwlkclwwlk  41211  clwlksfclwwlk  41269  frgrncvvdeqlemB  41477  frgr2wsp1  41495  frrusgrord0  41503  rngcl  41673  nzerooringczr  41864  ply1mulgsum  41972  sinhpcosh  42280  reseccl  42293  recsccl  42294  recotcl  42295  onetansqsecsq  42301