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  1431  syl3an1br  1434  wefrc  5652  tz7.5  6409  f1resrcmplf1dlem  7309  f1cdmsn  7321  f1ofvswap  7345  f1ofveu  7445  fovcdmda  7624  suppvalfng  8222  smoiso  8408  tz7.48lem  8488  odi  8625  nndi  8670  nnmsucr  8672  f1oen2g  9033  f1dom2g  9034  domssex2  9194  dif1ennn  9216  enfii  9239  phplem2  9258  php  9260  php3  9262  findcard3  9312  ordunifi  9319  nnsdomg  9329  rankfilimbi  9939  ackbij1lem16  10351  divneg  12048  divdiv32  12065  divneg2  12081  ltdiv2  12243  fimaxre  12301  fiminre  12304  suprzcl  12819  peano2uz  13068  infssuzle  13098  lbzbi  13103  zbtwnre  13113  irrmul  13142  supxrunb1  13489  expnlbnd  14418  hash1to3  14678  fun2dmnop  14691  brfi1uzind  14694  brcnvtrclfvcnv  15201  retancl  16354  tanneg  16360  demoivreALT  16413  dvdscmulr  16498  dvdsmulcr  16499  mulmoddvds  16544  gcd0id  16735  euclemma  16933  phiprmpw  16997  fermltl  17005  vdwapun  17196  vdwapid1  17197  cshwshashlem1  17317  fsets  17391  pospo  18567  tltnle  18644  latasymb  18666  mgmn0plusgf  18877  sgrpcl  18965  mndcl  18981  imasmnd2  19018  gsumsgrpccat  19086  grpcl  19202  dfgrp2  19223  grprcan  19234  grpsubcl  19280  imasgrp2  19315  mhmid  19323  mhmmnd  19324  mulginvcom  19359  mulgnndir  19363  mulgnnass  19369  qusgrp  19451  ghmmulg  19492  ghmrn  19493  ghmeqker  19507  gsumccatsymgsn  19691  ablcom  20064  ablinvadd  20072  mulgmhm  20092  mulgghm  20093  ghmcmn  20096  odadd1  20113  odadd2  20114  rngacl  20435  rngcl  20437  rngpropd  20447  srgcl  20470  srgacl  20482  srgcom  20483  ringcl  20528  crngcom  20529  ringacl  20558  pwspjmhmmgpd  20608  imasring  20611  irredlmul  20709  rhmadd  20769  rhmsub  20770  rhmmul  20771  subrngacl  20859  subrgacl  20886  subrgmcl  20887  subrgugrp  20894  isdomn4  21018  isdrngd  21073  isdrngdOLD  21075  ringen1zr0  21086  srngadd  21159  srngmul  21160  idsrngd  21164  lmodacl  21198  lmodmcl  21199  lmodvacl  21201  lmodvsubcl  21233  lmod4  21238  lmodvaddsub4  21240  lmodvpncan  21241  lmodvnpcan  21242  lmodsubeq0  21247  pwssplit3  21387  islbs2  21483  islbs3  21484  lbsext  21492  rspssp  21573  cringm4  21678  nzerooringczr  21841  zlmlmod  21883  psgnco  21944  ipdir  22000  ip2eq  22014  ocvin  22035  frlmsplit2  22134  ascldimul  22251  rnasclmulcl  22257  mplbas2  22406  coe1add  22638  coe1subfv  22640  coe1mul2  22643  rhmply1vsca  22758  ringvcl  22770  matunitlindflem1  23049  cramer  23064  chpmat1d  23209  filin  24228  filfinnfr  24251  filuni  24259  ufprim  24283  uffinfix  24301  hausflf  24371  uffcfflf  24413  cnextcn  24441  tmdmulg  24466  tsmsxplem1  24527  psmetcl  24681  xmetcl  24705  metcl  24706  meteq0  24713  metge0  24719  metsym  24724  metgt0  24733  blelrnps  24790  blelrn  24791  blssm  24792  blres  24805  mscl  24835  xmscl  24836  xmsge0  24837  xmseq0  24838  xmssym  24839  mopnin  24871  nmf2  24967  ngpdsr  24979  ngpds2  24980  ngpds2r  24981  ngpds3  24982  ngpds3r  24983  nmge0  24991  nmeq0  24992  nm2dif  24999  nmmul  25038  nlmmul0or  25057  nmods  25118  clmsub  25456  clmacl  25460  clmmcl  25461  clmsubcl  25462  clmvscl  25464  clmvsubval  25485  ncvsprp  25528  ncvsdif  25531  ncvspds  25537  cphnmvs  25566  cphipcl  25567  cphipcj  25575  cphorthcom  25577  cphipval2  25617  4cphipval2  25618  cphipval  25619  fmcfil  25648  mbfi1fseqlem3  26093  mbfi1fseqlem4  26094  mbfi1fseqlem5  26095  deg1ldgdomn  26467  drnguc1p  26547  quotval  26668  sincosq1sgn  26884  sincosq2sgn  26885  sincosq3sgn  26886  sincosq4sgn  26887  efabl  26935  lgsneg1  27706  dchrisumlem3  27875  bdayn0p1  28812  ax5seglem2  29564  usgredg2vtx  29857  uspgredg2vtxeu  29858  usgredg2vtxeu  29859  cplgr3v  30073  vtxdumgr0nedg  30131  swrdwlk  30325  clwlkclwwlk  30650  frgrncvvdeqlem8  30964  grpocl  31159  grpodivcl  31198  ablomuldiv  31211  ablodivdiv4  31213  ablonnncan1  31216  vccl  31222  nvgcl  31279  nvcom  31280  nvadd4  31284  nvscl  31285  nvmval  31301  nvmcl  31305  nmcvcn  31354  nmlnoubi  31455  isblo3i  31460  blometi  31462  dipsubdir  31507  hlpar2  31555  hlpar  31556  hlcom  31559  hlipcj  31570  hlipgt0  31573  his52  31746  shintcli  31988  chlub  32168  homulass  32461  adjadj  32595  nmophmi  32690  kbass6  32780  atcvatlem  33044  mdsymlem3  33064  mdsymlem5  33066  suppiniseg  33376  rexdiv  33588  tlt3  33627  toslublem  33629  tosglblem  33631  archiabllem1b  33852  archiabllem2  33857  slmdacl  33869  slmdmcl  33870  slmdvacl  33872  lidlincl  34084  evls1fldgencl  34413  aean  34988  fiunelcarsg  35059  probcun  35161  probdif  35163  cndprobin  35177  cusgredgex  36104  satefvfmla1  36398  climuzcnv  36644  pibt2  38608  mblfinlem1  38843  mblfinlem2  38844  ftc1anclem6  38884  ssbnd  38988  heibor1  39010  exidcl  39076  rngocl  39101  rngogcl  39112  rngocom  39113  rngoa4  39116  rngosub  39130  rngonegmn1l  39141  rngonegmn1r  39142  ispridlc  39270  lshpcmp  40311  opltcon3b  40527  oldmm1  40540  olj01  40548  latm32  40554  omllaw4  40569  omllaw5N  40570  cmtcomlemN  40571  cmt2N  40573  cmtbr2N  40576  cmtbr3N  40577  cmtbr4N  40578  glbconxN  40701  hlexch1  40705  hlexch2  40706  hlexchb1  40707  hlexchb2  40708  hlexch3  40714  hlexch4N  40715  hlatexchb1  40716  hlatexchb2  40717  hlatexch1  40718  hlatexch2  40719  hlatle  40721  hlateq  40722  hlrelat1  40723  hlrelat2  40726  cvr1  40733  cvrval5  40738  cvrp  40739  atcvr1  40740  atcvr2  40741  cvrexchlem  40742  cvrexch  40743  dalem54  41049  pmaple  41084  pmap11  41085  paddass  41161  pmapj2N  41252  pmapocjN  41253  trlval2  41486  nnproddivdvdsd  43316  fsuppssind  43887  mhphf  43891  0prjspnlem  43928  grumnudlem  45530  eelT00  45947  eelTTT  45948  eelT11  45949  eelT12  45951  eelTT1  45952  eelT01  45953  mullimc  46901  mullimcf  46908  dvmptfprod  47228  stoweidlem52  47335  stoweidlem60  47343  focofob  48423  f1ocof1ob  48424  clnbgrgrim  49305  ply1mulgsum  49833  itschlc0xyqsol1  50209  sinhpcosh  51238  reseccl  51274  recsccl  51275  recotcl  51276  onetansqsecsq  51282