Theorem 3coml 1237

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  3comr  1238  nndir  6736  f1oen2g  7007  f1dom2g  7008  ordiso  7340  addassnqg  7713  ltbtwnnqq  7746  nnanq0  7789  ltasrg  8101  recexgt0sr  8104  axmulass  8204  adddir  8281  axltadd  8359  ltleletr  8371  letr  8372  pnpcan2  8530  subdir  8677  div13ap  8987  zdiv  9687  xrletr  10163  fzen  10400  fzrevral2  10465  fzshftral  10467  fzind2  10610  mulbinom2  11045  ccatlcan  11438  elicc4abs  11808  dvdsnegb  12523  muldvds1  12531  muldvds2  12532  dvdscmul  12533  dvdsmulc  12534  dvdsgcd  12737  mulgcdr  12743  lcmgcdeq  12809  congr  12826  mulgnnass  13914  mettri  15368  cnmet  15525  addcncntoplem  15556