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  4390  f1ofveu  5906  fovcdmda  6062  smoiso  6355  tfrcl  6417  omv  6508  oeiv  6509  nndi  6539  nnmsucr  6541  f1oen2g  6809  f1dom2g  6810  undiffi  6981  prarloclemarch2  7479  distrnq0  7519  ltprordil  7649  1idprl  7650  1idpru  7651  ltpopr  7655  ltexprlemopu  7663  ltexprlemdisj  7666  ltexprlemfl  7669  ltexprlemfu  7671  ltexprlemru  7672  recexprlemdisj  7690  recexprlemss1l  7695  recexprlemss1u  7696  cnegexlem1  8194  msqge0  8635  mulge0  8638  divnegap  8725  divdiv32ap  8739  divneg2ap  8755  peano2uz  9648  lbzbi  9681  negqmod0  10402  modqmuladdnn0  10439  expnlbnd  10735  shftfvalg  10962  xrmaxaddlem  11403  retanclap  11865  tannegap  11871  demoivreALT  11917  gcd0id  12116  isprm3  12256  euclemma  12284  phiprmpw  12360  fermltl  12372  sgrpcl  12992  mndcl  13004  grpcl  13080  dfgrp2  13099  grprcan  13109  grpsubcl  13152  imasgrp2  13180  mhmid  13185  mhmmnd  13186  mulginvcom  13217  mulgnndir  13221  mulgnnass  13227  qusgrp  13302  ghmmulg  13326  ghmrn  13327  ghmeqker  13341  ablcom  13373  ablinvadd  13380  ghmcmn  13397  rngacl  13438  rngpropd  13451  srgacl  13478  srgcom  13479  ringacl  13526  imasring  13560  subrngacl  13704  subrgacl  13728  subrgugrp  13736  lmodacl  13795  lmodmcl  13796  lmodvacl  13798  lmodvsubcl  13828  lmod4  13833  lmodvaddsub4  13835  lmodvpncan  13836  lmodvnpcan  13837  lmodsubeq0  13842  psmetcl  14494  xmetcl  14520  metcl  14521  meteq0  14528  metge0  14534  metsym  14539  blelrnps  14587  blelrn  14588  blssm  14589  blres  14602  mscl  14633  xmscl  14634  xmsge0  14635  xmseq0  14636  xmssym  14637  mopnin  14655  sincosq1sgn  14961  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  lgsneg1  15141