Theorem syl3an1 1304

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

Syntax hints:   → wi 4   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  syl3an1b  1307  syl3an1br  1310  wepo  4450  f1ofveu  5995  fovcdmda  6155  smoiso  6454  tfrcl  6516  omv  6609  oeiv  6610  nndi  6640  nnmsucr  6642  f1oen2g  6914  f1dom2g  6915  undiffi  7098  prarloclemarch2  7617  distrnq0  7657  ltprordil  7787  1idprl  7788  1idpru  7789  ltpopr  7793  ltexprlemopu  7801  ltexprlemdisj  7804  ltexprlemfl  7807  ltexprlemfu  7809  ltexprlemru  7810  recexprlemdisj  7828  recexprlemss1l  7833  recexprlemss1u  7834  cnegexlem1  8332  msqge0  8774  mulge0  8777  divnegap  8864  divdiv32ap  8878  divneg2ap  8894  peano2uz  9790  lbzbi  9823  negqmod0  10565  modqmuladdnn0  10602  expnlbnd  10898  fun2dmnop  11083  shftfvalg  11344  xrmaxaddlem  11786  retanclap  12248  tannegap  12254  demoivreALT  12300  gcd0id  12515  isprm3  12655  euclemma  12683  phiprmpw  12759  fermltl  12771  sgrpcl  13457  mndcl  13471  imasmnd2  13500  grpcl  13556  dfgrp2  13575  grprcan  13585  grpsubcl  13628  imasgrp2  13662  mhmid  13667  mhmmnd  13668  mulginvcom  13699  mulgnndir  13703  mulgnnass  13709  qusgrp  13784  ghmmulg  13808  ghmrn  13809  ghmeqker  13823  ablcom  13855  ablinvadd  13862  ghmcmn  13879  rngacl  13920  rngpropd  13933  srgacl  13960  srgcom  13961  ringacl  14008  imasring  14042  subrngacl  14187  subrgacl  14211  subrgugrp  14219  lmodacl  14278  lmodmcl  14279  lmodvacl  14281  lmodvsubcl  14311  lmod4  14316  lmodvaddsub4  14318  lmodvpncan  14319  lmodvnpcan  14320  lmodsubeq0  14325  psmetcl  15015  xmetcl  15041  metcl  15042  meteq0  15049  metge0  15055  metsym  15060  blelrnps  15108  blelrn  15109  blssm  15110  blres  15123  mscl  15154  xmscl  15155  xmsge0  15156  xmseq0  15157  xmssym  15158  mopnin  15176  sincosq1sgn  15515  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  lgsneg1  15719  usgredg2vtx  16030  uspgredg2vtxeu  16031  usgredg2vtxeu  16032