Theorem 3comr 1237

Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3comr	⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem 3comr

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3coml 1236	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)
3	2	3coml 1236	1 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  nnacan  6680  le2tri3i  8288  ltaddsublt  8751  div12ap  8874  lemul12b  9041  zdivadd  9569  zdivmul  9570  elfz  10249  fzmmmeqm  10293  fzrev  10319  absdiflt  11657  absdifle  11658  dvds0lem  12367  dvdsmulc  12385  dvds2add  12391  dvds2sub  12392  dvdstr  12394  lcmdvds  12656  psmettri2  15058  xmettri2  15091