Theorem syl3an1 1181

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant1l  1195  3adant1r  1196  syl3an1b  1430  syl3an1br  1433  wefrc  5657  tz7.5  6385  f1resrcmplf1dlem  7274  f1cdmsn  7286  f1ofvswap  7310  f1ofveu  7410  fovcdmda  7587  suppvalfng  8165  smoiso  8351  odi  8566  nndi  8611  nnmsucr  8613  f1oen2g  8967  f1dom2g  8968  domssex2  9128  dif1ennn  9150  enfii  9173  phplem2  9192  php  9194  php3  9196  findcard3  9246  ordunifi  9253  nnsdomg  9262  ackbij1lem16  10229  divneg  11917  divdiv32  11934  divneg2  11950  ltdiv2  12112  fimaxre  12170  fiminre  12173  suprzcl  12688  peano2uz  12937  infssuzle  12967  lbzbi  12972  zbtwnre  12982  irrmul  13010  supxrunb1  13357  expnlbnd  14283  hash1to3  14543  fun2dmnop  14556  brfi1uzind  14559  brcnvtrclfvcnv  15062  retancl  16216  tanneg  16222  demoivreALT  16275  dvdscmulr  16360  dvdsmulcr  16361  mulmoddvds  16406  gcd0id  16595  euclemma  16790  phiprmpw  16853  fermltl  16861  vdwapun  17052  vdwapid1  17053  cshwshashlem1  17173  fsets  17247  pospo  18417  tltnle  18494  latasymb  18516  sgrpcl  18806  mndcl  18822  imasmnd2  18856  gsumsgrpccat  18923  grpcl  19032  dfgrp2  19053  grprcan  19064  grpsubcl  19110  imasgrp2  19145  mhmid  19153  mhmmnd  19154  mulginvcom  19189  mulgnndir  19193  mulgnnass  19199  qusgrp  19281  ghmmulg  19322  ghmrn  19323  ghmeqker  19337  gsumccatsymgsn  19520  ablcom  19893  ablinvadd  19901  mulgmhm  19921  mulgghm  19922  ghmcmn  19925  odadd1  19942  odadd2  19943  rngacl  20264  rngcl  20266  rngpropd  20276  srgcl  20299  srgacl  20311  srgcom  20312  ringcl  20356  crngcom  20357  ringacl  20386  pwspjmhmmgpd  20435  imasring  20438  irredlmul  20536  rhmadd  20596  rhmsub  20597  rhmmul  20598  subrngacl  20685  subrgacl  20712  subrgmcl  20713  subrgugrp  20720  isdomn4  20844  isdrngd  20898  isdrngdOLD  20900  ringen1zr0  20911  srngadd  20984  srngmul  20985  idsrngd  20989  lmodacl  21023  lmodmcl  21024  lmodvacl  21026  lmodvsubcl  21058  lmod4  21063  lmodvaddsub4  21065  lmodvpncan  21066  lmodvnpcan  21067  lmodsubeq0  21072  pwssplit3  21212  islbs2  21308  islbs3  21309  lbsext  21317  rspssp  21398  cringm4  21501  nzerooringczr  21660  zlmlmod  21702  psgnco  21763  ipdir  21819  ip2eq  21833  ocvin  21854  frlmsplit2  21953  ascldimul  22068  rnasclmulcl  22074  mplbas2  22223  coe1add  22455  coe1subfv  22457  coe1mul2  22460  rhmply1vsca  22575  ringvcl  22587  cramer  22878  chpmat1d  23023  filin  24042  filfinnfr  24065  filuni  24073  ufprim  24097  uffinfix  24115  hausflf  24185  uffcfflf  24227  cnextcn  24255  tmdmulg  24280  tsmsxplem1  24341  psmetcl  24495  xmetcl  24519  metcl  24520  meteq0  24527  metge0  24533  metsym  24538  metgt0  24547  blelrnps  24604  blelrn  24605  blssm  24606  blres  24619  mscl  24649  xmscl  24650  xmsge0  24651  xmseq0  24652  xmssym  24653  mopnin  24685  nmf2  24781  ngpdsr  24793  ngpds2  24794  ngpds2r  24795  ngpds3  24796  ngpds3r  24797  nmge0  24805  nmeq0  24806  nm2dif  24813  nmmul  24852  nlmmul0or  24871  nmods  24932  clmsub  25270  clmacl  25274  clmmcl  25275  clmsubcl  25276  clmvscl  25278  clmvsubval  25299  ncvsprp  25342  ncvsdif  25345  ncvspds  25351  cphnmvs  25380  cphipcl  25381  cphipcj  25389  cphorthcom  25391  cphipval2  25431  4cphipval2  25432  cphipval  25433  fmcfil  25462  mbfi1fseqlem3  25907  mbfi1fseqlem4  25908  mbfi1fseqlem5  25909  deg1ldgdomn  26282  drnguc1p  26362  quotval  26484  sincosq1sgn  26694  sincosq2sgn  26695  sincosq3sgn  26696  sincosq4sgn  26697  efabl  26746  lgsneg1  27517  dchrisumlem3  27686  bdayn0p1  28593  ax5seglem2  29310  usgredg2vtx  29603  uspgredg2vtxeu  29604  usgredg2vtxeu  29605  cplgr3v  29819  vtxdumgr0nedg  29877  swrdwlk  30071  clwlkclwwlk  30396  frgrncvvdeqlem8  30704  grpocl  30899  grpodivcl  30938  ablomuldiv  30951  ablodivdiv4  30953  ablonnncan1  30956  vccl  30962  nvgcl  31019  nvcom  31020  nvadd4  31024  nvscl  31025  nvmval  31041  nvmcl  31045  nmcvcn  31094  nmlnoubi  31195  isblo3i  31200  blometi  31202  dipsubdir  31247  hlpar2  31295  hlpar  31296  hlcom  31299  hlipcj  31310  hlipgt0  31313  his52  31486  shintcli  31728  chlub  31908  homulass  32201  adjadj  32335  nmophmi  32430  kbass6  32520  atcvatlem  32784  mdsymlem3  32804  mdsymlem5  32806  suppiniseg  33078  rexdiv  33291  tlt3  33330  toslublem  33332  tosglblem  33334  archiabllem1b  33552  archiabllem2  33557  slmdacl  33569  slmdmcl  33570  slmdvacl  33572  lidlincl  33778  evls1fldgencl  34100  aean  34675  fiunelcarsg  34747  probcun  34849  probdif  34851  cndprobin  34865  rankfilimbi  35529  cusgredgex  35640  satefvfmla1  35930  climuzcnv  36176  pibt2  38096  matunitlindflem1  38300  mblfinlem1  38341  mblfinlem2  38342  ftc1anclem6  38382  ssbnd  38472  heibor1  38494  exidcl  38560  rngocl  38585  rngogcl  38596  rngocom  38597  rngoa4  38600  rngosub  38614  rngonegmn1l  38625  rngonegmn1r  38626  ispridlc  38754  lshpcmp  39795  opltcon3b  40011  oldmm1  40024  olj01  40032  latm32  40038  omllaw4  40053  omllaw5N  40054  cmtcomlemN  40055  cmt2N  40057  cmtbr2N  40060  cmtbr3N  40061  cmtbr4N  40062  glbconxN  40185  hlexch1  40189  hlexch2  40190  hlexchb1  40191  hlexchb2  40192  hlexch3  40198  hlexch4N  40199  hlatexchb1  40200  hlatexchb2  40201  hlatexch1  40202  hlatexch2  40203  hlatle  40205  hlateq  40206  hlrelat1  40207  hlrelat2  40210  cvr1  40217  cvrval5  40222  cvrp  40223  atcvr1  40224  atcvr2  40225  cvrexchlem  40226  cvrexch  40227  dalem54  40533  pmaple  40568  pmap11  40569  paddass  40645  pmapj2N  40736  pmapocjN  40737  trlval2  40970  nnproddivdvdsd  42800  fsuppssind  43358  mhphf  43362  0prjspnlem  43388  grumnudlem  45028  eelT00  45446  eelTTT  45447  eelT11  45448  eelT12  45450  eelTT1  45451  eelT01  45452  mullimc  46365  mullimcf  46372  dvmptfprod  46692  stoweidlem52  46799  stoweidlem60  46807  focofob  47850  f1ocof1ob  47851  clnbgrgrim  48732  ply1mulgsum  49203  itschlc0xyqsol1  49579  sinhpcosh  50551  reseccl  50564  recsccl  50565  recotcl  50566  onetansqsecsq  50572