Theorem 3coml 1234

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

Syntax hints:   → wi 4   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  3comr  1235  nndir  6626  f1oen2g  6896  f1dom2g  6897  ordiso  7191  addassnqg  7557  ltbtwnnqq  7590  nnanq0  7633  ltasrg  7945  recexgt0sr  7948  axmulass  8048  adddir  8125  axltadd  8204  ltleletr  8216  letr  8217  pnpcan2  8374  subdir  8520  div13ap  8828  zdiv  9523  xrletr  9992  fzen  10227  fzrevral2  10290  fzshftral  10292  fzind2  10432  mulbinom2  10865  ccatlcan  11236  elicc4abs  11591  dvdsnegb  12305  muldvds1  12313  muldvds2  12314  dvdscmul  12315  dvdsmulc  12316  dvdsgcd  12519  mulgcdr  12525  lcmgcdeq  12591  congr  12608  mulgnnass  13680  mettri  15032  cnmet  15189  addcncntoplem  15220