Theorem syl3an3 1358

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

Ref	Expression
syl3an3.1	⊢ (𝜑 → 𝜃)
syl3an3.2	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3an3	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Proof of Theorem syl3an3

Step	Hyp	Ref	Expression
1		syl3an3.1	. . 3 ⊢ (𝜑 → 𝜃)
2		syl3an3.2	. . . 4 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
3	2	3exp 1261	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))
4	1, 3	syl7 74	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜏)))
5	4	3imp 1254	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038

This theorem is referenced by:  syl3an3b  1361  syl3an3br  1364  vtoclgftOLD  3241  disji  4600  ovmpt2x  6742  ovmpt2ga  6743  wfrlem14  7373  unbnn2  8161  axdc3lem4  9219  axdclem2  9286  gruiin  9576  gruen  9578  divass  10647  ltmul2  10818  xleadd1  12028  xltadd2  12030  xlemul1  12063  xltmul2  12066  elfzo  12413  modcyc2  12646  faclbnd5  13025  relexprel  13713  subcn2  14259  mulcn2  14260  ndvdsp1  15059  gcddiv  15192  lcmneg  15240  lubel  17043  gsumccatsn  17301  mulgaddcom  17485  oddvdsi  17888  odcong  17889  odeq  17890  efgsp1  18071  lspsnss  18909  lindsmm2  20087  mulmarep1el  20297  mdetunilem4  20340  iuncld  20759  neips  20827  opnneip  20833  comppfsc  21245  hmeof1o2  21476  ordthmeo  21515  ufinffr  21643  elfm3  21664  utop3cls  21965  blcntrps  22127  blcntr  22128  neibl  22216  blnei  22217  metss  22223  stdbdmetval  22229  prdsms  22246  blval2  22277  lmmbr  22964  lmmbr2  22965  iscau2  22983  bcthlem1  23029  bcthlem3  23031  bcthlem4  23032  dvn2bss  23599  dvfsumrlim  23698  dvfsumrlim2  23699  cxpexpz  24313  cxpsub  24328  relogbzexp  24414  upgr4cycl4dv4e  26911  konigsbergssiedgwpr  26976  hvaddsub12  27741  hvaddsubass  27744  hvsubdistr1  27752  hvsubcan  27777  hhssnv  27967  spanunsni  28284  homco1  28506  homulass  28507  hoadddir  28509  hosubdi  28513  hoaddsubass  28520  hosubsub4  28523  lnopmi  28705  adjlnop  28791  mdsymlem5  29112  disjif  29233  disjif2  29236  ind0  29860  sigaclfu  29960  bnj544  30669  bnj561  30678  bnj562  30679  bnj594  30687  clsint2  31963  ftc1anclem6  33119  isbnd2  33211  blbnd  33215  isdrngo2  33386  atnem0  34082  hlrelat5N  34164  ltrnel  34902  ltrnat  34903  ltrncnvat  34904  jm2.22  37039  jm2.23  37040  dvconstbi  38012  eelT11  38411  eelT12  38413  eelTT1  38414  eelT01  38415  eel0T1  38416  rmfsupp  41440  mndpfsupp  41442  scmfsupp  41444  dignn0flhalflem2  41699