Theorem syl3an2 1164

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

Hypotheses

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

Assertion

Ref	Expression
syl3an2	⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

Proof of Theorem syl3an2

Step	Hyp	Ref	Expression
1		syl3an2.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	3anim2i 1153	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an2.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 17	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3adant2l  1179  3adant2r  1180  syl3an2b  1406  syl3an2br  1409  fviunfun  7886  odi  8503  omass  8504  nndi  8547  nnmass  8548  omabslem  8574  domtrfil  9112  domnsymfi  9120  sdomdomtrfi  9121  domsdomtrfi  9122  php  9127  php3  9129  f1finf1o  9168  findcard3  9178  winainf  10596  divsubdir  11826  divdiv32  11840  ltdiv2  12019  peano2uz  12805  irrmul  12878  supxrunb1  13225  fzoshftral  13694  ltdifltdiv  13745  axdc4uzlem  13897  expdiv  14027  bcval5  14232  rediv  15045  imdiv  15052  absdiflt  15232  absdifle  15233  iseraltlem3  15598  retancl  16058  tanneg  16064  difmod0  16205  lcmgcdeq  16530  prmdvdsexpb  16634  dvdsprmpweqnn  16804  mulgaddcomlem  19018  mulginvcom  19020  pmtrfb  19385  lspssp  20930  mdetunilem7  22553  m2detleiblem3  22564  m2detleiblem4  22565  pmatcollpw  22716  pmatcollpwscmat  22726  chpmatply1  22767  chfacfscmulgsum  22795  chfacfpmmulcl  22796  chfacfpmmul0  22797  chfacfpmmulgsum  22799  chfacfpmmulgsum2  22800  cayhamlem1  22801  cpmadurid  22802  cpmadugsumlemC  22810  cpmadugsumlemF  22811  cpmadugsumfi  22812  cpmidgsum2  22814  islp2  23080  fmfg  23884  fmufil  23894  flffbas  23930  lmflf  23940  uffcfflf  23974  blres  24366  ncvsge0  25100  caucfil  25230  cmetcusp1  25300  deg1mul3  26068  quotval  26247  sltonold  28218  cusgr3vnbpr  29435  clwwlkinwwlk  30041  nvsge0  30665  hvsubass  31045  hvsubdistr2  31051  hvsubcan  31075  his2sub  31093  chlub  31510  spanunsni  31580  homco1  31802  homulass  31803  cnlnadjlem2  32069  adjmul  32093  chirredlem2  32392  atmd2  32401  mdsymlem5  32408  f1resrcmplf1dlem  35170  revpfxsfxrev  35232  climuzcnv  35787  pibt2  37534  f1ocan2fv  37840  isdrngo2  38071  atncvrN  39487  cvlatcvr1  39513  eluzrabdioph  42963  iocmbl  43370  rp-isfinite6  43675  ismnushort  44458  dvconstbi  44491  eelT11  44863  eelT12  44865  eelTT1  44866  eel0T1  44868  nn0digval  48762  dignn0flhalf  48780  sinhpcosh  49901  reseccl  49914  recsccl  49915  recotcl  49916  onetansqsecsq  49922