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  3582  omwordri  8584  oeword  8602  f1oen2g  8983  f1dom2g  8984  f1imaenfi  9209  ordiso  9530  en3lplem2  9627  axdc3lem4  10467  ltasr  11114  adddir  11226  axltadd  11308  pnpcan2  11523  subdir  11671  ltaddsub  11711  leaddsub  11713  mulcan2g  11891  div13  11917  ltdiv2  12128  lediv2  12132  zdiv  12663  xadddir  13312  xadddi2r  13314  fzen  13558  fzrevral2  13630  fzshftral  13632  ssfzoulel  13776  fzind2  13801  flflp1  13824  mulbinom2  14241  digit1  14255  faclbnd5  14316  ccatlcan  14736  elicc4abs  15338  dvdsnegb  16293  muldvds1  16300  muldvds2  16301  dvdscmul  16302  dvdsmulc  16303  dvdscmulr  16304  dvdsmulcr  16305  dvdsgcd  16563  mulgcdr  16569  lcmgcdeq  16631  congr  16683  mulgnnass  19092  gaass  19280  elfm3  23888  mettri  24291  cnmet  24710  addcnlem  24804  bcthlem5  25280  isppw2  27077  vmappw  27078  bcmono  27240  sletr  27722  sltadd1im  27944  colinearalg  28889  ax5seglem1  28907  ax5seglem2  28908  vcdir  30547  vcass  30548  imsmetlem  30671  hvaddcan2  31052  hvsubcan2  31056  dfgcd3  37342  isbasisrelowllem1  37373  ltflcei  37632  fzmul  37765  brcnvrabga  38360  pclfinclN  39969  rabrenfdioph  42837  uun123p2  44834  isosctrlem1ALT  44958