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  3572  omwordri  8539  oeword  8557  f1oen2g  8943  f1dom2g  8944  f1imaenfi  9165  ordiso  9476  en3lplem2  9573  axdc3lem4  10413  ltasr  11060  adddir  11172  axltadd  11254  pnpcan2  11469  subdir  11619  ltaddsub  11659  leaddsub  11661  mulcan2g  11839  div13  11865  ltdiv2  12076  lediv2  12080  zdiv  12611  xadddir  13263  xadddi2r  13265  fzen  13509  fzrevral2  13581  fzshftral  13583  ssfzoulel  13728  fzind2  13753  flflp1  13776  mulbinom2  14195  digit1  14209  faclbnd5  14270  ccatlcan  14690  elicc4abs  15293  dvdsnegb  16250  muldvds1  16257  muldvds2  16258  dvdscmul  16259  dvdsmulc  16260  dvdscmulr  16261  dvdsmulcr  16262  dvdsgcd  16521  mulgcdr  16527  lcmgcdeq  16589  congr  16641  mulgnnass  19048  gaass  19236  elfm3  23844  mettri  24247  cnmet  24666  addcnlem  24760  bcthlem5  25235  isppw2  27032  vmappw  27033  bcmono  27195  sletr  27677  sltadd1im  27899  colinearalg  28844  ax5seglem1  28862  ax5seglem2  28863  vcdir  30502  vcass  30503  imsmetlem  30626  hvaddcan2  31007  hvsubcan2  31011  dfgcd3  37319  isbasisrelowllem1  37350  ltflcei  37609  fzmul  37742  brcnvrabga  38331  pclfinclN  39951  rabrenfdioph  42809  uun123p2  44806  isosctrlem1ALT  44930