Theorem 3coml 1292

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

Syntax hints:   → wi 4   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  3comrOLD  1294  omwordri  7697  oeword  7715  f1oen2g  8014  f1dom2g  8015  ordiso  8462  en3lplem2  8550  axdc3lem4  9313  ltasr  9959  adddir  10069  axltadd  10149  pnpcan2  10359  subdir  10502  ltaddsub  10540  leaddsub  10542  mulcan2g  10719  div13  10744  ltdiv2  10947  lediv2  10951  zdiv  11485  xadddir  12164  xadddi2r  12166  fzen  12396  fzrevral2  12464  fzshftral  12466  ssfzoulel  12602  fzind2  12626  flflp1  12648  mulbinom2  13024  digit1  13038  faclbnd5  13125  ccatlcan  13518  relexpreld  13824  elicc4abs  14103  dvdsnegb  15046  muldvds1  15053  muldvds2  15054  dvdscmul  15055  dvdsmulc  15056  dvdscmulr  15057  dvdsmulcr  15058  dvdsgcd  15308  mulgcdr  15314  lcmgcdeq  15372  coprmdvdsOLD  15414  congr  15425  mulgnnass  17623  mulgnnassOLD  17624  gaass  17776  elfm3  21801  mettri  22204  cnmet  22622  addcnlem  22714  bcthlem5  23171  isppw2  24886  vmappw  24887  bcmono  25047  colinearalg  25835  ax5seglem1  25853  ax5seglem2  25854  vcdir  27549  vcass  27550  imsmetlem  27673  hvaddcan2  28056  hvsubcan2  28060  sletr  32008  dfgcd3  33300  isbasisrelowllem1  33333  ltflcei  33527  fzmul  33667  pclfinclN  35554  rabrenfdioph  37695  uun123p2  39354  isosctrlem1ALT  39484