Theorem 3coml 1143

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 1142	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)
3	2	3com13 1140	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  spc3egv  3565  omwordri  8545  oeword  8564  f1oen2g  8953  f1dom2g  8954  f1imaenfi  9167  ordiso  9466  en3lplem2  9570  axdc3lem4  10425  ltasr  11073  adddir  11185  axltadd  11271  pnpcan2  11486  subdir  11636  ltaddsub  11676  leaddsub  11678  mulcan2g  11856  div13  11881  ltdiv2  12092  lediv2  12096  zdiv  12657  xadddir  13313  xadddi2r  13315  fzen  13560  fzrevral2  13632  fzshftral  13634  ssfzoulel  13780  fzind2  13808  flflp1  13831  mulbinom2  14250  digit1  14264  faclbnd5  14325  ccatlcan  14745  elicc4abs  15361  dvdsnegb  16321  muldvds1  16328  muldvds2  16329  dvdscmul  16330  dvdsmulc  16331  dvdscmulr  16332  dvdsmulcr  16333  dvdsgcd  16592  mulgcdr  16598  lcmgcdeq  16660  congr  16712  mulgnnass  19166  gaass  19358  elfm3  24068  mettri  24470  cnmet  24889  addcnlem  24983  bcthlem5  25448  isppw2  27237  vmappw  27238  bcmono  27399  lestr  27884  ltadds1im  28136  colinearalg  29169  ax5seglem1  29187  ax5seglem2  29188  vcdir  30827  vcass  30828  imsmetlem  30951  hvaddcan2  31332  hvsubcan2  31336  dfgcd3  37828  isbasisrelowllem1  37861  ltflcei  38119  fzmul  38252  brcnvrabga  38853  pclfinclN  40586  rabrenfdioph  43403  uun123p2  45383  isosctrlem1ALT  45507