Theorem syl3an1 1163

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3adant1l  1177  3adant1r  1178  syl3an1b  1405  syl3an1br  1408  wefrc  5635  tz7.5  6356  f1cdmsn  7260  f1ofvswap  7284  f1ofveu  7384  fovcdmda  7563  suppvalfng  8149  smoiso  8334  odi  8546  nndi  8590  nnmsucr  8592  f1oen2g  8943  f1dom2g  8944  domssex2  9107  dif1ennn  9131  enfii  9156  phplem2  9175  php  9177  php3  9179  findcard3  9236  ordunifi  9244  nnsdomg  9253  ackbij1lem16  10194  divneg  11881  divdiv32  11897  divneg2  11913  ltdiv2  12076  fimaxre  12134  fiminre  12137  suprzcl  12621  peano2uz  12867  infssuzle  12897  lbzbi  12902  zbtwnre  12912  irrmul  12940  supxrunb1  13286  expnlbnd  14205  hash1to3  14464  fun2dmnop  14477  brfi1uzind  14480  brcnvtrclfvcnv  14978  retancl  16117  tanneg  16123  demoivreALT  16176  dvdscmulr  16261  dvdsmulcr  16262  mulmoddvds  16307  gcd0id  16496  euclemma  16690  phiprmpw  16753  fermltl  16761  vdwapun  16952  vdwapid1  16953  cshwshashlem1  17073  fsets  17146  pospo  18311  tltnle  18388  latasymb  18408  sgrpcl  18660  mndcl  18676  imasmnd2  18708  gsumsgrpccat  18774  grpcl  18880  dfgrp2  18901  grprcan  18912  grpsubcl  18959  imasgrp2  18994  mhmid  19002  mhmmnd  19003  mulginvcom  19038  mulgnndir  19042  mulgnnass  19048  qusgrp  19125  ghmmulg  19167  ghmrn  19168  ghmeqker  19182  gsumccatsymgsn  19363  ablcom  19736  ablinvadd  19744  mulgmhm  19764  mulgghm  19765  ghmcmn  19768  odadd1  19785  odadd2  19786  rngacl  20078  rngcl  20080  rngpropd  20090  srgcl  20109  srgacl  20121  srgcom  20122  ringcl  20166  crngcom  20167  ringacl  20194  pwspjmhmmgpd  20244  imasring  20246  irredlmul  20344  rhmmul  20402  subrngacl  20472  subrgacl  20499  subrgmcl  20500  subrgugrp  20507  isdomn4  20632  drngmclOLD  20667  isdrngd  20681  isdrngdOLD  20683  srngadd  20767  srngmul  20768  idsrngd  20772  lmodacl  20785  lmodmcl  20786  lmodvacl  20788  lmodvsubcl  20820  lmod4  20825  lmodvaddsub4  20827  lmodvpncan  20828  lmodvnpcan  20829  lmodsubeq0  20834  pwssplit3  20975  islbs2  21071  islbs3  21072  lbsext  21080  rspssp  21156  nzerooringczr  21397  zlmlmod  21439  psgnco  21499  ipdir  21555  ip2eq  21569  ocvin  21590  frlmsplit2  21689  ascldimul  21804  rnasclmulcl  21810  mplbas2  21956  coe1add  22157  coe1subfv  22159  coe1mul2  22162  rhmply1vsca  22282  ringvcl  22294  cramer  22585  chpmat1d  22730  filin  23748  filfinnfr  23771  filuni  23779  ufprim  23803  uffinfix  23821  hausflf  23891  uffcfflf  23933  cnextcn  23961  tmdmulg  23986  tsmsxplem1  24047  psmetcl  24202  xmetcl  24226  metcl  24227  meteq0  24234  metge0  24240  metsym  24245  metgt0  24254  blelrnps  24311  blelrn  24312  blssm  24313  blres  24326  mscl  24356  xmscl  24357  xmsge0  24358  xmseq0  24359  xmssym  24360  mopnin  24392  nmf2  24488  ngpdsr  24500  ngpds2  24501  ngpds2r  24502  ngpds3  24503  ngpds3r  24504  nmge0  24512  nmeq0  24513  nm2dif  24520  nmmul  24559  nlmmul0or  24578  nmods  24639  clmsub  24987  clmacl  24991  clmmcl  24992  clmsubcl  24993  clmvscl  24995  clmvsubval  25016  ncvsprp  25059  ncvsdif  25062  ncvspds  25068  cphnmvs  25097  cphipcl  25098  cphipcj  25106  cphorthcom  25108  cphipval2  25148  4cphipval2  25149  cphipval  25150  fmcfil  25179  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  deg1ldgdomn  26006  drnguc1p  26086  quotval  26207  sincosq1sgn  26414  sincosq2sgn  26415  sincosq3sgn  26416  sincosq4sgn  26417  efabl  26466  lgsneg1  27240  dchrisumlem3  27409  bdayn0p1  28265  ax5seglem2  28863  usgredg2vtx  29153  uspgredg2vtxeu  29154  usgredg2vtxeu  29155  cplgr3v  29369  vtxdumgr0nedg  29428  clwlkclwwlk  29938  frgrncvvdeqlem8  30242  grpocl  30436  grpodivcl  30475  ablomuldiv  30488  ablodivdiv4  30490  ablonnncan1  30493  vccl  30499  nvgcl  30556  nvcom  30557  nvadd4  30561  nvscl  30562  nvmval  30578  nvmcl  30582  nmcvcn  30631  nmlnoubi  30732  isblo3i  30737  blometi  30739  dipsubdir  30784  hlpar2  30832  hlpar  30833  hlcom  30836  hlipcj  30847  hlipgt0  30850  his52  31023  shintcli  31265  chlub  31445  homulass  31738  adjadj  31872  nmophmi  31967  kbass6  32057  atcvatlem  32321  mdsymlem3  32341  mdsymlem5  32343  suppiniseg  32616  rexdiv  32853  tlt3  32903  toslublem  32905  tosglblem  32907  archiabllem1b  33153  archiabllem2  33158  slmdacl  33169  slmdmcl  33170  slmdvacl  33172  lidlincl  33408  cringm4  33424  evls1fldgencl  33672  aean  34241  fiunelcarsg  34314  probcun  34416  probdif  34418  cndprobin  34432  f1resrcmplf1dlem  35083  cusgredgex  35116  swrdwlk  35121  satefvfmla1  35419  climuzcnv  35665  pibt2  37412  matunitlindflem1  37617  mblfinlem1  37658  mblfinlem2  37659  ftc1anclem6  37699  ssbnd  37789  heibor1  37811  exidcl  37877  rngocl  37902  rngogcl  37913  rngocom  37914  rngoa4  37917  rngosub  37931  rngonegmn1l  37942  rngonegmn1r  37943  ispridlc  38071  lshpcmp  38988  opltcon3b  39204  oldmm1  39217  olj01  39225  latm32  39231  omllaw4  39246  omllaw5N  39247  cmtcomlemN  39248  cmt2N  39250  cmtbr2N  39253  cmtbr3N  39254  cmtbr4N  39255  glbconxN  39379  hlexch1  39383  hlexch2  39384  hlexchb1  39385  hlexchb2  39386  hlexch3  39392  hlexch4N  39393  hlatexchb1  39394  hlatexchb2  39395  hlatexch1  39396  hlatexch2  39397  hlatle  39399  hlateq  39400  hlrelat1  39401  hlrelat2  39404  cvr1  39411  cvrval5  39416  cvrp  39417  atcvr1  39418  atcvr2  39419  cvrexchlem  39420  cvrexch  39421  dalem54  39727  pmaple  39762  pmap11  39763  paddass  39839  pmapj2N  39930  pmapocjN  39931  trlval2  40164  nnproddivdvdsd  41995  fsuppssind  42588  mhphf  42592  0prjspnlem  42618  grumnudlem  44281  eelT00  44701  eelTTT  44702  eelT11  44703  eelT12  44705  eelTT1  44706  eelT01  44707  mullimc  45621  mullimcf  45628  dvmptfprod  45950  stoweidlem52  46057  stoweidlem60  46065  focofob  47085  f1ocof1ob  47086  clnbgrgrim  47938  ply1mulgsum  48383  itschlc0xyqsol1  48759  sinhpcosh  49733  reseccl  49746  recsccl  49747  recotcl  49748  onetansqsecsq  49754