Theorem 3coml 1127

Description: Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3coml	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)

Proof of Theorem 3coml

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3com23 1126	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)
3	2	3com13 1124	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:  spc3egv  3560  omwordri  8497  oeword  8515  f1oen2g  8901  f1dom2g  8902  f1imaenfi  9119  ordiso  9427  en3lplem2  9528  axdc3lem4  10366  ltasr  11013  adddir  11125  axltadd  11207  pnpcan2  11422  subdir  11572  ltaddsub  11612  leaddsub  11614  mulcan2g  11792  div13  11818  ltdiv2  12029  lediv2  12033  zdiv  12564  xadddir  13216  xadddi2r  13218  fzen  13462  fzrevral2  13534  fzshftral  13536  ssfzoulel  13681  fzind2  13706  flflp1  13729  mulbinom2  14148  digit1  14162  faclbnd5  14223  ccatlcan  14642  elicc4abs  15245  dvdsnegb  16202  muldvds1  16209  muldvds2  16210  dvdscmul  16211  dvdsmulc  16212  dvdscmulr  16213  dvdsmulcr  16214  dvdsgcd  16473  mulgcdr  16479  lcmgcdeq  16541  congr  16593  mulgnnass  19006  gaass  19194  elfm3  23853  mettri  24256  cnmet  24675  addcnlem  24769  bcthlem5  25244  isppw2  27041  vmappw  27042  bcmono  27204  sletr  27686  sltadd1im  27915  colinearalg  28873  ax5seglem1  28891  ax5seglem2  28892  vcdir  30528  vcass  30529  imsmetlem  30652  hvaddcan2  31033  hvsubcan2  31037  dfgcd3  37297  isbasisrelowllem1  37328  ltflcei  37587  fzmul  37720  brcnvrabga  38309  pclfinclN  39929  rabrenfdioph  42787  uun123p2  44783  isosctrlem1ALT  44907