Theorem 3coml 1126

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 1125	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)
3	2	3com13 1123	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  3603  omwordri  8609  oeword  8627  f1oen2g  9008  f1dom2g  9009  f1imaenfi  9233  ordiso  9554  en3lplem2  9651  axdc3lem4  10491  ltasr  11138  adddir  11250  axltadd  11332  pnpcan2  11547  subdir  11695  ltaddsub  11735  leaddsub  11737  mulcan2g  11915  div13  11941  ltdiv2  12152  lediv2  12156  zdiv  12686  xadddir  13335  xadddi2r  13337  fzen  13578  fzrevral2  13650  fzshftral  13652  ssfzoulel  13796  fzind2  13821  flflp1  13844  mulbinom2  14259  digit1  14273  faclbnd5  14334  ccatlcan  14753  elicc4abs  15355  dvdsnegb  16308  muldvds1  16315  muldvds2  16316  dvdscmul  16317  dvdsmulc  16318  dvdscmulr  16319  dvdsmulcr  16320  dvdsgcd  16578  mulgcdr  16584  lcmgcdeq  16646  congr  16698  mulgnnass  19140  gaass  19328  elfm3  23974  mettri  24378  cnmet  24808  addcnlem  24900  bcthlem5  25376  isppw2  27173  vmappw  27174  bcmono  27336  sletr  27818  sltadd1im  28033  colinearalg  28940  ax5seglem1  28958  ax5seglem2  28959  vcdir  30595  vcass  30596  imsmetlem  30719  hvaddcan2  31100  hvsubcan2  31104  dfgcd3  37307  isbasisrelowllem1  37338  ltflcei  37595  fzmul  37728  brcnvrabga  38324  pclfinclN  39933  rabrenfdioph  42802  uun123p2  44808  isosctrlem1ALT  44932