Theorem syl3an1 1271

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  syl3an1b  1274  syl3an1br  1277  wepo  4361  f1ofveu  5865  fovcdmda  6020  smoiso  6305  tfrcl  6367  omv  6458  oeiv  6459  nndi  6489  nnmsucr  6491  f1oen2g  6757  f1dom2g  6758  undiffi  6926  prarloclemarch2  7420  distrnq0  7460  ltprordil  7590  1idprl  7591  1idpru  7592  ltpopr  7596  ltexprlemopu  7604  ltexprlemdisj  7607  ltexprlemfl  7610  ltexprlemfu  7612  ltexprlemru  7613  recexprlemdisj  7631  recexprlemss1l  7636  recexprlemss1u  7637  cnegexlem1  8134  msqge0  8575  mulge0  8578  divnegap  8665  divdiv32ap  8679  divneg2ap  8695  peano2uz  9585  lbzbi  9618  negqmod0  10333  modqmuladdnn0  10370  expnlbnd  10647  shftfvalg  10829  xrmaxaddlem  11270  retanclap  11732  tannegap  11738  demoivreALT  11783  gcd0id  11982  isprm3  12120  euclemma  12148  phiprmpw  12224  fermltl  12236  mndcl  12829  grpcl  12890  dfgrp2  12907  grprcan  12915  grpsubcl  12955  mhmid  12984  mhmmnd  12985  mulginvcom  13013  mulgnndir  13017  mulgnnass  13023  ablcom  13111  ablinvadd  13118  srgacl  13170  srgcom  13171  ringacl  13218  subrgacl  13358  subrgugrp  13366  lmodacl  13394  lmodmcl  13395  lmodvacl  13397  lmodvsubcl  13427  lmod4  13432  lmodvaddsub4  13434  lmodvpncan  13435  lmodvnpcan  13436  lmodsubeq0  13441  psmetcl  13911  xmetcl  13937  metcl  13938  meteq0  13945  metge0  13951  metsym  13956  blelrnps  14004  blelrn  14005  blssm  14006  blres  14019  mscl  14050  xmscl  14051  xmsge0  14052  xmseq0  14053  xmssym  14054  mopnin  14072  sincosq1sgn  14332  sincosq2sgn  14333  sincosq3sgn  14334  sincosq4sgn  14335  lgsneg1  14511