Theorem 3comr 1147

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 1146	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)
3	2	3coml 1146	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:  nnacan  6151  le2tri3i  7286  ltaddsublt  7738  div12ap  7849  lemul12b  8006  zdivadd  8517  zdivmul  8518  elfz  9111  fzmmmeqm  9152  fzrev  9177  absdiflt  10116  absdifle  10117  dvds0lem  10350  dvdsmulc  10368  dvds2add  10374  dvds2sub  10375  dvdstr  10377  lcmdvds  10605