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

This theorem is referenced by:  spc3egv  3552  omwordri  8181  oeword  8199  f1oen2g  8509  f1dom2g  8510  ordiso  8964  en3lplem2  9060  axdc3lem4  9864  ltasr  10511  adddir  10621  axltadd  10703  pnpcan2  10915  subdir  11063  ltaddsub  11103  leaddsub  11105  mulcan2g  11283  div13  11308  ltdiv2  11515  lediv2  11519  zdiv  12040  xadddir  12677  xadddi2r  12679  fzen  12919  fzrevral2  12988  fzshftral  12990  ssfzoulel  13126  fzind2  13150  flflp1  13172  mulbinom2  13580  digit1  13594  faclbnd5  13654  ccatlcan  14071  elicc4abs  14671  dvdsnegb  15619  muldvds1  15626  muldvds2  15627  dvdscmul  15628  dvdsmulc  15629  dvdscmulr  15630  dvdsmulcr  15631  dvdsgcd  15882  mulgcdr  15888  lcmgcdeq  15946  congr  15998  mulgnnass  18254  gaass  18419  elfm3  22555  mettri  22959  cnmet  23377  addcnlem  23469  bcthlem5  23932  isppw2  25700  vmappw  25701  bcmono  25861  colinearalg  26704  ax5seglem1  26722  ax5seglem2  26723  vcdir  28349  vcass  28350  imsmetlem  28473  hvaddcan2  28854  hvsubcan2  28858  sletr  33350  dfgcd3  34738  isbasisrelowllem1  34772  ltflcei  35045  fzmul  35179  brcnvrabga  35759  pclfinclN  37246  rabrenfdioph  39755  uun123p2  41516  isosctrlem1ALT  41640