Theorem syl3an3 1353

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 1256	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))
4	1, 3	syl7 72	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜏)))
5	4	3imp 1249	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  syl3an3b  1356  syl3an3br  1359  vtoclgftOLD  3228  disji  4570  ovmpt2x  6687  ovmpt2ga  6688  wfrlem14  7315  unbnn2  8102  axdc3lem4  9158  axdclem2  9225  gruiin  9511  gruen  9513  divass  10582  ltmul2  10753  xleadd1  11957  xltadd2  11959  xlemul1  11992  xltmul2  11995  elfzo  12341  modcyc2  12568  faclbnd5  12947  relexprel  13627  subcn2  14173  mulcn2  14174  ndvdsp1  14973  gcddiv  15106  lcmneg  15154  lubel  16945  gsumccatsn  17203  mulgaddcom  17387  oddvdsi  17790  odcong  17791  odeq  17792  efgsp1  17973  lspsnss  18811  lindsmm2  19987  mulmarep1el  20197  mdetunilem4  20240  iuncld  20659  neips  20727  opnneip  20733  comppfsc  21145  hmeof1o2  21376  ordthmeo  21415  ufinffr  21543  elfm3  21564  utop3cls  21865  blcntrps  22027  blcntr  22028  neibl  22116  blnei  22117  metss  22123  stdbdmetval  22129  prdsms  22146  blval2  22177  lmmbr  22864  lmmbr2  22865  iscau2  22883  bcthlem1  22929  bcthlem3  22931  bcthlem4  22932  dvn2bss  23499  dvfsumrlim  23598  dvfsumrlim2  23599  cxpexpz  24213  cxpsub  24228  relogbzexp  24314  wlkcompim  26054  wwlknext  26252  wwlkextproplem3  26271  clwlkcompim  26292  clwwlkel  26321  clwwlkf  26322  numclwlk1lem2f1  26621  hvaddsub12  27279  hvaddsubass  27282  hvsubdistr1  27290  hvsubcan  27315  hhssnv  27505  spanunsni  27822  homco1  28044  homulass  28045  hoadddir  28047  hosubdi  28051  hoaddsubass  28058  hosubsub4  28061  lnopmi  28243  adjlnop  28329  mdsymlem5  28650  disjif  28773  disjif2  28776  ind0  29409  sigaclfu  29509  bnj544  30218  bnj561  30227  bnj562  30228  bnj594  30236  clsint2  31494  ftc1anclem6  32660  isbnd2  32752  blbnd  32756  isdrngo2  32927  atnem0  33623  hlrelat5N  33705  ltrnel  34443  ltrnat  34444  ltrncnvat  34445  jm2.22  36580  jm2.23  36581  dvconstbi  37555  eelT11  37953  eelT12  37955  eelTT1  37956  eelT01  37957  eel0T1  37958  upgr4cycl4dv4e  41352  konigsbergssiedgwpr  41418  rmfsupp  41949  mndpfsupp  41951  scmfsupp  41953  dignn0flhalflem2  42208