Theorem syl3an1 1306

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  syl3an1b  1309  syl3an1br  1312  wepo  4456  f1ofveu  6006  fovcdmda  6166  smoiso  6468  tfrcl  6530  omv  6623  oeiv  6624  nndi  6654  nnmsucr  6656  f1oen2g  6928  f1dom2g  6929  undiffi  7117  prarloclemarch2  7639  distrnq0  7679  ltprordil  7809  1idprl  7810  1idpru  7811  ltpopr  7815  ltexprlemopu  7823  ltexprlemdisj  7826  ltexprlemfl  7829  ltexprlemfu  7831  ltexprlemru  7832  recexprlemdisj  7850  recexprlemss1l  7855  recexprlemss1u  7856  cnegexlem1  8354  msqge0  8796  mulge0  8799  divnegap  8886  divdiv32ap  8900  divneg2ap  8916  peano2uz  9817  lbzbi  9850  negqmod0  10594  modqmuladdnn0  10631  expnlbnd  10927  fun2dmnop  11116  shftfvalg  11383  xrmaxaddlem  11825  retanclap  12288  tannegap  12294  demoivreALT  12340  gcd0id  12555  isprm3  12695  euclemma  12723  phiprmpw  12799  fermltl  12811  sgrpcl  13497  mndcl  13511  imasmnd2  13540  grpcl  13596  dfgrp2  13615  grprcan  13625  grpsubcl  13668  imasgrp2  13702  mhmid  13707  mhmmnd  13708  mulginvcom  13739  mulgnndir  13743  mulgnnass  13749  qusgrp  13824  ghmmulg  13848  ghmrn  13849  ghmeqker  13863  ablcom  13895  ablinvadd  13902  ghmcmn  13919  rngacl  13961  rngpropd  13974  srgacl  14001  srgcom  14002  ringacl  14049  imasring  14083  subrngacl  14228  subrgacl  14252  subrgugrp  14260  lmodacl  14319  lmodmcl  14320  lmodvacl  14322  lmodvsubcl  14352  lmod4  14357  lmodvaddsub4  14359  lmodvpncan  14360  lmodvnpcan  14361  lmodsubeq0  14366  psmetcl  15056  xmetcl  15082  metcl  15083  meteq0  15090  metge0  15096  metsym  15101  blelrnps  15149  blelrn  15150  blssm  15151  blres  15164  mscl  15195  xmscl  15196  xmsge0  15197  xmseq0  15198  xmssym  15199  mopnin  15217  sincosq1sgn  15556  sincosq2sgn  15557  sincosq3sgn  15558  sincosq4sgn  15559  lgsneg1  15760  usgredg2vtx  16074  uspgredg2vtxeu  16075  usgredg2vtxeu  16076