Theorem syl3an1 1282

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  syl3an1b  1285  syl3an1br  1288  wepo  4395  f1ofveu  5913  fovcdmda  6071  smoiso  6369  tfrcl  6431  omv  6522  oeiv  6523  nndi  6553  nnmsucr  6555  f1oen2g  6823  f1dom2g  6824  undiffi  6995  prarloclemarch2  7503  distrnq0  7543  ltprordil  7673  1idprl  7674  1idpru  7675  ltpopr  7679  ltexprlemopu  7687  ltexprlemdisj  7690  ltexprlemfl  7693  ltexprlemfu  7695  ltexprlemru  7696  recexprlemdisj  7714  recexprlemss1l  7719  recexprlemss1u  7720  cnegexlem1  8218  msqge0  8660  mulge0  8663  divnegap  8750  divdiv32ap  8764  divneg2ap  8780  peano2uz  9674  lbzbi  9707  negqmod0  10440  modqmuladdnn0  10477  expnlbnd  10773  shftfvalg  11000  xrmaxaddlem  11442  retanclap  11904  tannegap  11910  demoivreALT  11956  gcd0id  12171  isprm3  12311  euclemma  12339  phiprmpw  12415  fermltl  12427  sgrpcl  13111  mndcl  13125  imasmnd2  13154  grpcl  13210  dfgrp2  13229  grprcan  13239  grpsubcl  13282  imasgrp2  13316  mhmid  13321  mhmmnd  13322  mulginvcom  13353  mulgnndir  13357  mulgnnass  13363  qusgrp  13438  ghmmulg  13462  ghmrn  13463  ghmeqker  13477  ablcom  13509  ablinvadd  13516  ghmcmn  13533  rngacl  13574  rngpropd  13587  srgacl  13614  srgcom  13615  ringacl  13662  imasring  13696  subrngacl  13840  subrgacl  13864  subrgugrp  13872  lmodacl  13931  lmodmcl  13932  lmodvacl  13934  lmodvsubcl  13964  lmod4  13969  lmodvaddsub4  13971  lmodvpncan  13972  lmodvnpcan  13973  lmodsubeq0  13978  psmetcl  14646  xmetcl  14672  metcl  14673  meteq0  14680  metge0  14686  metsym  14691  blelrnps  14739  blelrn  14740  blssm  14741  blres  14754  mscl  14785  xmscl  14786  xmsge0  14787  xmseq0  14788  xmssym  14789  mopnin  14807  sincosq1sgn  15146  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  lgsneg1  15350