Theorem syl3an2 1352

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

Hypotheses

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

Assertion

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

Proof of Theorem syl3an2

Step	Hyp	Ref	Expression
1		syl3an2.1	. . 3 ⊢ (𝜑 → 𝜒)
2		syl3an2.2	. . . 4 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
3	2	3exp 1256	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))
4	1, 3	syl5 33	. 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:  syl3an2b  1355  syl3an2br  1358  syl3anl2  1367  odi  7546  omass  7547  nndi  7590  nnmass  7591  omabslem  7613  winainf  9395  divsubdir  10600  divdiv32  10612  ltdiv2  10788  peano2uz  11617  irrmul  11689  supxrunb1  12021  fzoshftral  12447  ltdifltdiv  12497  axdc4uzlem  12644  expdiv  12773  bcval5  12967  ccats1val1  13255  rediv  13719  imdiv  13726  absdiflt  13905  absdifle  13906  iseraltlem3  14262  retancl  14711  tanneg  14717  lcmgcdeq  15163  prmdvdsexpb  15266  dvdsprmpweqnn  15427  mulgaddcomlem  17386  mulginvcom  17388  pmtrfb  17708  lspssp  18809  mdetunilem7  20243  m2detleiblem3  20254  m2detleiblem4  20255  pmatcollpw  20405  pmatcollpwscmat  20415  chpmatply1  20456  chfacfscmulgsum  20484  chfacfpmmulcl  20485  chfacfpmmul0  20486  chfacfpmmulgsum  20488  chfacfpmmulgsum2  20489  cayhamlem1  20490  cpmadurid  20491  cpmadugsumlemC  20499  cpmadugsumlemF  20500  cpmadugsumfi  20501  cpmidgsum2  20503  islp2  20759  fmfg  21563  fmufil  21573  flffbas  21609  lmflf  21619  uffcfflf  21653  blres  22046  ncvsge0  22761  caucfil  22889  cmetcusp1  22957  deg1mul3  23679  quotval  23851  cusgra3vnbpr  25994  nvsge0  26903  hvsubass  27285  hvsubdistr2  27291  hvsubcan  27315  his2sub  27333  chlub  27752  spanunsni  27822  homco1  28044  homulass  28045  cnlnadjlem2  28311  adjmul  28335  chirredlem2  28634  atmd2  28643  mdsymlem5  28650  climuzcnv  30819  f1ocan2fv  32692  isdrngo2  32927  atncvrN  33620  cvlatcvr1  33646  eluzrabdioph  36388  iocmbl  36817  rp-isfinite6  36883  dvconstbi  37555  eelT11  37953  eelT12  37955  eelTT1  37956  eel0T1  37958  cusgr3vnbpr  40658  nn0digval  42192  dignn0flhalf  42210  sinhpcosh  42280  reseccl  42293  recsccl  42294  recotcl  42295  onetansqsecsq  42301