Theorem 3coml 1146

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

Syntax hints:   → wi 4   ∧ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  3comr  1147  nndir  6182  f1oen2g  6401  f1dom2g  6402  ordiso  6635  addassnqg  6843  ltbtwnnqq  6876  nnanq0  6919  ltasrg  7218  recexgt0sr  7221  axmulass  7310  adddir  7381  axltadd  7458  ltleletr  7469  letr  7470  pnpcan2  7624  subdir  7766  div13ap  8057  zdiv  8729  xrletr  9167  fzen  9351  fzrevral2  9412  fzshftral  9414  fzind2  9538  mulbinom2  9904  elicc4abs  10353  dvdsnegb  10592  muldvds1  10600  muldvds2  10601  dvdscmul  10602  dvdsmulc  10603  dvdsgcd  10780  mulgcdr  10786  lcmgcdeq  10844  congr  10861