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  3569  omwordri  8536  oeword  8554  f1oen2g  8940  f1dom2g  8941  f1imaenfi  9159  ordiso  9469  en3lplem2  9566  axdc3lem4  10406  ltasr  11053  adddir  11165  axltadd  11247  pnpcan2  11462  subdir  11612  ltaddsub  11652  leaddsub  11654  mulcan2g  11832  div13  11858  ltdiv2  12069  lediv2  12073  zdiv  12604  xadddir  13256  xadddi2r  13258  fzen  13502  fzrevral2  13574  fzshftral  13576  ssfzoulel  13721  fzind2  13746  flflp1  13769  mulbinom2  14188  digit1  14202  faclbnd5  14263  ccatlcan  14683  elicc4abs  15286  dvdsnegb  16243  muldvds1  16250  muldvds2  16251  dvdscmul  16252  dvdsmulc  16253  dvdscmulr  16254  dvdsmulcr  16255  dvdsgcd  16514  mulgcdr  16520  lcmgcdeq  16582  congr  16634  mulgnnass  19041  gaass  19229  elfm3  23837  mettri  24240  cnmet  24659  addcnlem  24753  bcthlem5  25228  isppw2  27025  vmappw  27026  bcmono  27188  sletr  27670  sltadd1im  27892  colinearalg  28837  ax5seglem1  28855  ax5seglem2  28856  vcdir  30495  vcass  30496  imsmetlem  30619  hvaddcan2  31000  hvsubcan2  31004  dfgcd3  37312  isbasisrelowllem1  37343  ltflcei  37602  fzmul  37735  brcnvrabga  38324  pclfinclN  39944  rabrenfdioph  42802  uun123p2  44799  isosctrlem1ALT  44923