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  5645  tz7.5  6382  f1resrcmplf1dlem  7276  f1cdmsn  7288  f1ofvswap  7312  f1ofveu  7412  fovcdmda  7590  suppvalfng  8177  smoiso  8363  tz7.48lem  8443  odi  8580  nndi  8625  nnmsucr  8627  f1oen2g  8988  f1dom2g  8989  domssex2  9149  dif1ennn  9171  enfii  9194  phplem2  9213  php  9215  php3  9217  findcard3  9267  ordunifi  9274  nnsdomg  9284  rankfilimbi  9895  ackbij1lem16  10305  divneg  12001  divdiv32  12018  divneg2  12034  ltdiv2  12196  fimaxre  12254  fiminre  12257  suprzcl  12772  peano2uz  13021  infssuzle  13051  lbzbi  13056  zbtwnre  13066  irrmul  13095  supxrunb1  13442  expnlbnd  14370  hash1to3  14630  fun2dmnop  14643  brfi1uzind  14646  brcnvtrclfvcnv  15151  retancl  16303  tanneg  16309  demoivreALT  16362  dvdscmulr  16447  dvdsmulcr  16448  mulmoddvds  16493  gcd0id  16684  euclemma  16882  phiprmpw  16946  fermltl  16954  vdwapun  17145  vdwapid1  17146  cshwshashlem1  17266  fsets  17340  pospo  18510  tltnle  18587  latasymb  18609  mgmn0plusgf  18820  sgrpcl  18908  mndcl  18924  imasmnd2  18961  gsumsgrpccat  19029  grpcl  19145  dfgrp2  19166  grprcan  19177  grpsubcl  19223  imasgrp2  19258  mhmid  19266  mhmmnd  19267  mulginvcom  19302  mulgnndir  19306  mulgnnass  19312  qusgrp  19394  ghmmulg  19435  ghmrn  19436  ghmeqker  19450  gsumccatsymgsn  19633  ablcom  20006  ablinvadd  20014  mulgmhm  20034  mulgghm  20035  ghmcmn  20038  odadd1  20055  odadd2  20056  rngacl  20377  rngcl  20379  rngpropd  20389  srgcl  20412  srgacl  20424  srgcom  20425  ringcl  20470  crngcom  20471  ringacl  20500  pwspjmhmmgpd  20550  imasring  20553  irredlmul  20651  rhmadd  20711  rhmsub  20712  rhmmul  20713  subrngacl  20801  subrgacl  20828  subrgmcl  20829  subrgugrp  20836  isdomn4  20960  isdrngd  21015  isdrngdOLD  21017  ringen1zr0  21028  srngadd  21101  srngmul  21102  idsrngd  21106  lmodacl  21140  lmodmcl  21141  lmodvacl  21143  lmodvsubcl  21175  lmod4  21180  lmodvaddsub4  21182  lmodvpncan  21183  lmodvnpcan  21184  lmodsubeq0  21189  pwssplit3  21329  islbs2  21425  islbs3  21426  lbsext  21434  rspssp  21515  cringm4  21620  nzerooringczr  21779  zlmlmod  21821  psgnco  21882  ipdir  21938  ip2eq  21952  ocvin  21973  frlmsplit2  22072  ascldimul  22189  rnasclmulcl  22195  mplbas2  22344  coe1add  22576  coe1subfv  22578  coe1mul2  22581  rhmply1vsca  22696  ringvcl  22708  matunitlindflem1  22987  cramer  23002  chpmat1d  23147  filin  24166  filfinnfr  24189  filuni  24197  ufprim  24221  uffinfix  24239  hausflf  24309  uffcfflf  24351  cnextcn  24379  tmdmulg  24404  tsmsxplem1  24465  psmetcl  24619  xmetcl  24643  metcl  24644  meteq0  24651  metge0  24657  metsym  24662  metgt0  24671  blelrnps  24728  blelrn  24729  blssm  24730  blres  24743  mscl  24773  xmscl  24774  xmsge0  24775  xmseq0  24776  xmssym  24777  mopnin  24809  nmf2  24905  ngpdsr  24917  ngpds2  24918  ngpds2r  24919  ngpds3  24920  ngpds3r  24921  nmge0  24929  nmeq0  24930  nm2dif  24937  nmmul  24976  nlmmul0or  24995  nmods  25056  clmsub  25394  clmacl  25398  clmmcl  25399  clmsubcl  25400  clmvscl  25402  clmvsubval  25423  ncvsprp  25466  ncvsdif  25469  ncvspds  25475  cphnmvs  25504  cphipcl  25505  cphipcj  25513  cphorthcom  25515  cphipval2  25555  4cphipval2  25556  cphipval  25557  fmcfil  25586  mbfi1fseqlem3  26031  mbfi1fseqlem4  26032  mbfi1fseqlem5  26033  deg1ldgdomn  26405  drnguc1p  26485  quotval  26606  sincosq1sgn  26820  sincosq2sgn  26821  sincosq3sgn  26822  sincosq4sgn  26823  efabl  26871  lgsneg1  27642  dchrisumlem3  27811  bdayn0p1  28748  ax5seglem2  29500  usgredg2vtx  29793  uspgredg2vtxeu  29794  usgredg2vtxeu  29795  cplgr3v  30009  vtxdumgr0nedg  30067  swrdwlk  30261  clwlkclwwlk  30586  frgrncvvdeqlem8  30900  grpocl  31095  grpodivcl  31134  ablomuldiv  31147  ablodivdiv4  31149  ablonnncan1  31152  vccl  31158  nvgcl  31215  nvcom  31216  nvadd4  31220  nvscl  31221  nvmval  31237  nvmcl  31241  nmcvcn  31290  nmlnoubi  31391  isblo3i  31396  blometi  31398  dipsubdir  31443  hlpar2  31491  hlpar  31492  hlcom  31495  hlipcj  31506  hlipgt0  31509  his52  31682  shintcli  31924  chlub  32104  homulass  32397  adjadj  32531  nmophmi  32626  kbass6  32716  atcvatlem  32980  mdsymlem3  33000  mdsymlem5  33002  suppiniseg  33272  rexdiv  33485  tlt3  33524  toslublem  33526  tosglblem  33528  archiabllem1b  33746  archiabllem2  33751  slmdacl  33763  slmdmcl  33764  slmdvacl  33766  lidlincl  33973  evls1fldgencl  34295  aean  34870  fiunelcarsg  34941  probcun  35043  probdif  35045  cndprobin  35059  cusgredgex  35885  satefvfmla1  36169  climuzcnv  36415  pibt2  38320  mblfinlem1  38555  mblfinlem2  38556  ftc1anclem6  38596  ssbnd  38702  heibor1  38724  exidcl  38790  rngocl  38815  rngogcl  38826  rngocom  38827  rngoa4  38830  rngosub  38844  rngonegmn1l  38855  rngonegmn1r  38856  ispridlc  38984  lshpcmp  40025  opltcon3b  40241  oldmm1  40254  olj01  40262  latm32  40268  omllaw4  40283  omllaw5N  40284  cmtcomlemN  40285  cmt2N  40287  cmtbr2N  40290  cmtbr3N  40291  cmtbr4N  40292  glbconxN  40415  hlexch1  40419  hlexch2  40420  hlexchb1  40421  hlexchb2  40422  hlexch3  40428  hlexch4N  40429  hlatexchb1  40430  hlatexchb2  40431  hlatexch1  40432  hlatexch2  40433  hlatle  40435  hlateq  40436  hlrelat1  40437  hlrelat2  40440  cvr1  40447  cvrval5  40452  cvrp  40453  atcvr1  40454  atcvr2  40455  cvrexchlem  40456  cvrexch  40457  dalem54  40763  pmaple  40798  pmap11  40799  paddass  40875  pmapj2N  40966  pmapocjN  40967  trlval2  41200  nnproddivdvdsd  43030  fsuppssind  43601  mhphf  43605  0prjspnlem  43642  grumnudlem  45254  eelT00  45672  eelTTT  45673  eelT11  45674  eelT12  45676  eelTT1  45677  eelT01  45678  mullimc  46597  mullimcf  46604  dvmptfprod  46924  stoweidlem52  47031  stoweidlem60  47039  focofob  48119  f1ocof1ob  48120  clnbgrgrim  49001  ply1mulgsum  49471  itschlc0xyqsol1  49847  sinhpcosh  50802  reseccl  50815  recsccl  50816  recotcl  50817  onetansqsecsq  50823