Theorem 3coml 1161

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

Syntax hints:   → wi 4   ∧ w3a 1111

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 199  df-an 387  df-3an 1113

This theorem is referenced by:  3comrOLD  1454  omwordri  7924  oeword  7942  f1oen2g  8245  f1dom2g  8246  ordiso  8697  en3lplem2  8792  axdc3lem4  9597  ltasr  10244  adddir  10354  axltadd  10437  pnpcan2  10649  subdir  10795  ltaddsub  10833  leaddsub  10835  mulcan2g  11013  div13  11038  ltdiv2  11246  lediv2  11250  zdiv  11782  xadddir  12421  xadddi2r  12423  fzen  12658  fzrevral2  12727  fzshftral  12729  ssfzoulel  12864  fzind2  12888  flflp1  12910  mulbinom2  13285  digit1  13299  faclbnd5  13385  ccatlcan  13814  relexpreld  14164  elicc4abs  14443  dvdsnegb  15383  muldvds1  15390  muldvds2  15391  dvdscmul  15392  dvdsmulc  15393  dvdscmulr  15394  dvdsmulcr  15395  dvdsgcd  15641  mulgcdr  15647  lcmgcdeq  15705  congr  15757  mulgnnass  17935  gaass  18087  elfm3  22131  mettri  22534  cnmet  22952  addcnlem  23044  bcthlem5  23503  isppw2  25261  vmappw  25262  bcmono  25422  colinearalg  26216  ax5seglem1  26234  ax5seglem2  26235  vcdir  27972  vcass  27973  imsmetlem  28096  hvaddcan2  28479  hvsubcan2  28483  sletr  32417  dfgcd3  33711  isbasisrelowllem1  33743  ltflcei  33935  fzmul  34074  brcnvrabga  34653  pclfinclN  36020  rabrenfdioph  38217  uun123p2  39859  isosctrlem1ALT  39983