Theorem 3coml 1124

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  spc3egv  3587  omwordri  8593  oeword  8611  f1oen2g  8989  f1dom2g  8990  f1dom2gOLD  8991  f1imaenfi  9226  ordiso  9546  en3lplem2  9643  axdc3lem4  10483  ltasr  11130  adddir  11242  axltadd  11324  pnpcan2  11537  subdir  11685  ltaddsub  11725  leaddsub  11727  mulcan2g  11905  div13  11931  ltdiv2  12138  lediv2  12142  zdiv  12670  xadddir  13315  xadddi2r  13317  fzen  13558  fzrevral2  13627  fzshftral  13629  ssfzoulel  13766  fzind2  13791  flflp1  13813  mulbinom2  14226  digit1  14240  faclbnd5  14298  ccatlcan  14709  elicc4abs  15307  dvdsnegb  16259  muldvds1  16266  muldvds2  16267  dvdscmul  16268  dvdsmulc  16269  dvdscmulr  16270  dvdsmulcr  16271  dvdsgcd  16528  mulgcdr  16534  lcmgcdeq  16591  congr  16643  mulgnnass  19077  gaass  19265  elfm3  23903  mettri  24307  cnmet  24737  addcnlem  24829  bcthlem5  25305  isppw2  27097  vmappw  27098  bcmono  27260  sletr  27742  sltadd1im  27953  colinearalg  28798  ax5seglem1  28816  ax5seglem2  28817  vcdir  30453  vcass  30454  imsmetlem  30577  hvaddcan2  30958  hvsubcan2  30962  dfgcd3  36936  isbasisrelowllem1  36967  ltflcei  37214  fzmul  37347  brcnvrabga  37946  pclfinclN  39555  rabrenfdioph  42378  uun123p2  44393  isosctrlem1ALT  44517