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 1087

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 1089

This theorem is referenced by:  spc3egv  3616  omwordri  8628  oeword  8646  f1oen2g  9028  f1dom2g  9029  f1dom2gOLD  9030  f1imaenfi  9261  ordiso  9585  en3lplem2  9682  axdc3lem4  10522  ltasr  11169  adddir  11281  axltadd  11363  pnpcan2  11576  subdir  11724  ltaddsub  11764  leaddsub  11766  mulcan2g  11944  div13  11970  ltdiv2  12181  lediv2  12185  zdiv  12713  xadddir  13358  xadddi2r  13360  fzen  13601  fzrevral2  13670  fzshftral  13672  ssfzoulel  13810  fzind2  13835  flflp1  13858  mulbinom2  14272  digit1  14286  faclbnd5  14347  ccatlcan  14766  elicc4abs  15368  dvdsnegb  16322  muldvds1  16329  muldvds2  16330  dvdscmul  16331  dvdsmulc  16332  dvdscmulr  16333  dvdsmulcr  16334  dvdsgcd  16591  mulgcdr  16597  lcmgcdeq  16659  congr  16711  mulgnnass  19149  gaass  19337  elfm3  23979  mettri  24383  cnmet  24813  addcnlem  24905  bcthlem5  25381  isppw2  27176  vmappw  27177  bcmono  27339  sletr  27821  sltadd1im  28036  colinearalg  28943  ax5seglem1  28961  ax5seglem2  28962  vcdir  30598  vcass  30599  imsmetlem  30722  hvaddcan2  31103  hvsubcan2  31107  dfgcd3  37290  isbasisrelowllem1  37321  ltflcei  37568  fzmul  37701  brcnvrabga  38298  pclfinclN  39907  rabrenfdioph  42770  uun123p2  44781  isosctrlem1ALT  44905