Theorem 3coml 1125

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  spc3egv  3532  omwordri  8365  oeword  8383  f1oen2g  8711  f1dom2g  8712  f1dom2gOLD  8713  f1imaenfi  8939  ordiso  9205  en3lplem2  9301  axdc3lem4  10140  ltasr  10787  adddir  10897  axltadd  10979  pnpcan2  11191  subdir  11339  ltaddsub  11379  leaddsub  11381  mulcan2g  11559  div13  11584  ltdiv2  11791  lediv2  11795  zdiv  12320  xadddir  12959  xadddi2r  12961  fzen  13202  fzrevral2  13271  fzshftral  13273  ssfzoulel  13409  fzind2  13433  flflp1  13455  mulbinom2  13866  digit1  13880  faclbnd5  13940  ccatlcan  14359  elicc4abs  14959  dvdsnegb  15911  muldvds1  15918  muldvds2  15919  dvdscmul  15920  dvdsmulc  15921  dvdscmulr  15922  dvdsmulcr  15923  dvdsgcd  16180  mulgcdr  16186  lcmgcdeq  16245  congr  16297  mulgnnass  18653  gaass  18818  elfm3  23009  mettri  23413  cnmet  23841  addcnlem  23933  bcthlem5  24397  isppw2  26169  vmappw  26170  bcmono  26330  colinearalg  27181  ax5seglem1  27199  ax5seglem2  27200  vcdir  28829  vcass  28830  imsmetlem  28953  hvaddcan2  29334  hvsubcan2  29338  sletr  33888  dfgcd3  35422  isbasisrelowllem1  35453  ltflcei  35692  fzmul  35826  brcnvrabga  36404  pclfinclN  37891  rabrenfdioph  40552  uun123p2  42319  isosctrlem1ALT  42443