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 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3adant1l  1195  3adant1r  1196  syl3an1b  1430  syl3an1br  1433  wefrc  5655  tz7.5  6381  f1cdmsn  7280  f1ofvswap  7304  f1ofveu  7404  fovcdmda  7581  suppvalfng  8159  smoiso  8345  odi  8560  nndi  8605  nnmsucr  8607  f1oen2g  8961  f1dom2g  8962  domssex2  9121  dif1ennn  9143  enfii  9166  phplem2  9185  php  9187  php3  9189  findcard3  9239  ordunifi  9246  nnsdomg  9255  ackbij1lem16  10213  divneg  11901  divdiv32  11918  divneg2  11934  ltdiv2  12096  fimaxre  12154  fiminre  12157  suprzcl  12671  peano2uz  12920  infssuzle  12950  lbzbi  12955  zbtwnre  12965  irrmul  12993  supxrunb1  13340  expnlbnd  14265  hash1to3  14525  fun2dmnop  14538  brfi1uzind  14541  brcnvtrclfvcnv  15038  retancl  16193  tanneg  16199  demoivreALT  16252  dvdscmulr  16337  dvdsmulcr  16338  mulmoddvds  16383  gcd0id  16572  euclemma  16767  phiprmpw  16830  fermltl  16838  vdwapun  17029  vdwapid1  17030  cshwshashlem1  17150  fsets  17224  pospo  18394  tltnle  18471  latasymb  18493  sgrpcl  18779  mndcl  18795  imasmnd2  18827  gsumsgrpccat  18894  grpcl  19003  dfgrp2  19024  grprcan  19035  grpsubcl  19081  imasgrp2  19116  mhmid  19124  mhmmnd  19125  mulginvcom  19160  mulgnndir  19164  mulgnnass  19170  qusgrp  19252  ghmmulg  19293  ghmrn  19294  ghmeqker  19308  gsumccatsymgsn  19491  ablcom  19864  ablinvadd  19872  mulgmhm  19892  mulgghm  19893  ghmcmn  19896  odadd1  19913  odadd2  19914  rngacl  20235  rngcl  20237  rngpropd  20247  srgcl  20270  srgacl  20282  srgcom  20283  ringcl  20327  crngcom  20328  ringacl  20357  pwspjmhmmgpd  20405  imasring  20408  irredlmul  20506  rhmadd  20566  rhmsub  20567  rhmmul  20568  subrngacl  20655  subrgacl  20682  subrgmcl  20683  subrgugrp  20690  isdomn4  20814  isdrngd  20868  isdrngdOLD  20870  ringen1zr0  20881  srngadd  20954  srngmul  20955  idsrngd  20959  lmodacl  20993  lmodmcl  20994  lmodvacl  20996  lmodvsubcl  21028  lmod4  21033  lmodvaddsub4  21035  lmodvpncan  21036  lmodvnpcan  21037  lmodsubeq0  21042  pwssplit3  21182  islbs2  21278  islbs3  21279  lbsext  21287  rspssp  21368  cringm4  21471  nzerooringczr  21630  zlmlmod  21672  psgnco  21733  ipdir  21789  ip2eq  21803  ocvin  21824  frlmsplit2  21923  ascldimul  22038  rnasclmulcl  22044  mplbas2  22193  coe1add  22425  coe1subfv  22427  coe1mul2  22430  rhmply1vsca  22545  ringvcl  22557  cramer  22848  chpmat1d  22993  filin  24011  filfinnfr  24034  filuni  24042  ufprim  24066  uffinfix  24084  hausflf  24154  uffcfflf  24196  cnextcn  24224  tmdmulg  24249  tsmsxplem1  24310  psmetcl  24464  xmetcl  24488  metcl  24489  meteq0  24496  metge0  24502  metsym  24507  metgt0  24516  blelrnps  24573  blelrn  24574  blssm  24575  blres  24588  mscl  24618  xmscl  24619  xmsge0  24620  xmseq0  24621  xmssym  24622  mopnin  24654  nmf2  24750  ngpdsr  24762  ngpds2  24763  ngpds2r  24764  ngpds3  24765  ngpds3r  24766  nmge0  24774  nmeq0  24775  nm2dif  24782  nmmul  24821  nlmmul0or  24840  nmods  24901  clmsub  25239  clmacl  25243  clmmcl  25244  clmsubcl  25245  clmvscl  25247  clmvsubval  25268  ncvsprp  25311  ncvsdif  25314  ncvspds  25320  cphnmvs  25349  cphipcl  25350  cphipcj  25358  cphorthcom  25360  cphipval2  25400  4cphipval2  25401  cphipval  25402  fmcfil  25431  mbfi1fseqlem3  25876  mbfi1fseqlem4  25877  mbfi1fseqlem5  25878  deg1ldgdomn  26251  drnguc1p  26331  quotval  26453  sincosq1sgn  26663  sincosq2sgn  26664  sincosq3sgn  26665  sincosq4sgn  26666  efabl  26715  lgsneg1  27486  dchrisumlem3  27655  bdayn0p1  28562  ax5seglem2  29279  usgredg2vtx  29569  uspgredg2vtxeu  29570  usgredg2vtxeu  29571  cplgr3v  29785  vtxdumgr0nedg  29843  clwlkclwwlk  30353  frgrncvvdeqlem8  30657  grpocl  30852  grpodivcl  30891  ablomuldiv  30904  ablodivdiv4  30906  ablonnncan1  30909  vccl  30915  nvgcl  30972  nvcom  30973  nvadd4  30977  nvscl  30978  nvmval  30994  nvmcl  30998  nmcvcn  31047  nmlnoubi  31148  isblo3i  31153  blometi  31155  dipsubdir  31200  hlpar2  31248  hlpar  31249  hlcom  31252  hlipcj  31263  hlipgt0  31266  his52  31439  shintcli  31681  chlub  31861  homulass  32154  adjadj  32288  nmophmi  32383  kbass6  32473  atcvatlem  32737  mdsymlem3  32757  mdsymlem5  32759  suppiniseg  33031  rexdiv  33245  tlt3  33290  toslublem  33292  tosglblem  33294  archiabllem1b  33512  archiabllem2  33517  slmdacl  33529  slmdmcl  33530  slmdvacl  33532  lidlincl  33738  evls1fldgencl  34060  aean  34634  fiunelcarsg  34706  probcun  34808  probdif  34810  cndprobin  34824  f1resrcmplf1dlem  35474  rankfilimbi  35495  cusgredgex  35614  swrdwlk  35619  satefvfmla1  35917  climuzcnv  36163  pibt2  38063  matunitlindflem1  38267  mblfinlem1  38308  mblfinlem2  38309  ftc1anclem6  38349  ssbnd  38439  heibor1  38461  exidcl  38527  rngocl  38552  rngogcl  38563  rngocom  38564  rngoa4  38567  rngosub  38581  rngonegmn1l  38592  rngonegmn1r  38593  ispridlc  38721  lshpcmp  39762  opltcon3b  39978  oldmm1  39991  olj01  39999  latm32  40005  omllaw4  40020  omllaw5N  40021  cmtcomlemN  40022  cmt2N  40024  cmtbr2N  40027  cmtbr3N  40028  cmtbr4N  40029  glbconxN  40152  hlexch1  40156  hlexch2  40157  hlexchb1  40158  hlexchb2  40159  hlexch3  40165  hlexch4N  40166  hlatexchb1  40167  hlatexchb2  40168  hlatexch1  40169  hlatexch2  40170  hlatle  40172  hlateq  40173  hlrelat1  40174  hlrelat2  40177  cvr1  40184  cvrval5  40189  cvrp  40190  atcvr1  40191  atcvr2  40192  cvrexchlem  40193  cvrexch  40194  dalem54  40500  pmaple  40535  pmap11  40536  paddass  40612  pmapj2N  40703  pmapocjN  40704  trlval2  40937  nnproddivdvdsd  42767  fsuppssind  43325  mhphf  43329  0prjspnlem  43355  grumnudlem  44995  eelT00  45413  eelTTT  45414  eelT11  45415  eelT12  45417  eelTT1  45418  eelT01  45419  mullimc  46332  mullimcf  46339  dvmptfprod  46659  stoweidlem52  46766  stoweidlem60  46774  focofob  47817  f1ocof1ob  47818  clnbgrgrim  48699  ply1mulgsum  49170  itschlc0xyqsol1  49546  sinhpcosh  50518  reseccl  50531  recsccl  50532  recotcl  50533  onetansqsecsq  50539