Theorem syl3an3 1170

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)

Hypotheses

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

Assertion

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

Proof of Theorem syl3an3

Step	Hyp	Ref	Expression
1		syl3an3.1	. . 3 ⊢ (𝜑 → 𝜃)
2	1	3anim3i 1158	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an3.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 17	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1072

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

This theorem is referenced by:  3adant3l  1194  3adant3r  1196  syl3an3b  1512  syl3an3br  1515  vtoclgftOLD  3391  disji  4785  ovmpt2x  6950  ovmpt2ga  6951  wfrlem14  7593  unbnn2  8378  axdc3lem4  9463  axdclem2  9530  gruiin  9820  gruen  9822  divass  10891  ltmul2  11062  xleadd1  12274  xltadd2  12276  xlemul1  12309  xltmul2  12312  elfzo  12662  modcyc2  12896  faclbnd5  13275  relexprel  13974  subcn2  14520  mulcn2  14521  ndvdsp1  15333  gcddiv  15466  lcmneg  15514  lubel  17319  gsumccatsn  17577  mulgaddcom  17761  oddvdsi  18163  odcong  18164  odeq  18165  efgsp1  18346  lspsnss  19188  lindsmm2  20366  mulmarep1el  20576  mdetunilem4  20619  iuncld  21047  neips  21115  opnneip  21121  comppfsc  21533  hmeof1o2  21764  ordthmeo  21803  ufinffr  21930  elfm3  21951  utop3cls  22252  blcntrps  22414  blcntr  22415  neibl  22503  blnei  22504  metss  22510  stdbdmetval  22516  prdsms  22533  blval2  22564  lmmbr  23252  lmmbr2  23253  iscau2  23271  bcthlem1  23317  bcthlem3  23319  bcthlem4  23320  dvn2bss  23888  dvfsumrlim  23989  dvfsumrlim2  23990  cxpexpz  24608  cxpsub  24623  relogbzexp  24709  upgr4cycl4dv4e  27333  konigsbergssiedgwpr  27397  dlwwlknondlwlknonf1o  27522  hvaddsub12  28200  hvaddsubass  28203  hvsubdistr1  28211  hvsubcan  28236  hhssnv  28426  spanunsni  28743  homco1  28965  homulass  28966  hoadddir  28968  hosubdi  28972  hoaddsubass  28979  hosubsub4  28982  lnopmi  29164  adjlnop  29250  mdsymlem5  29571  disjif  29694  disjif2  29697  ind0  30385  sigaclfu  30487  bnj544  31267  bnj561  31276  bnj562  31277  bnj594  31285  clsint2  32626  ftc1anclem6  33799  isbnd2  33891  blbnd  33895  isdrngo2  34066  atnem0  35104  hlrelat5N  35186  ltrnel  35924  ltrnat  35925  ltrncnvat  35926  jm2.22  38060  jm2.23  38061  dvconstbi  39031  eelT11  39430  eelT12  39432  eelTT1  39433  eelT01  39434  eel0T1  39435  liminfvalxr  40514  rmfsupp  42661  mndpfsupp  42663  scmfsupp  42665  dignn0flhalflem2  42916