Theorem 3comr 1190

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

Syntax hints:   → wi 4   ∧ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  nnacan  6416  le2tri3i  7896  ltaddsublt  8357  div12ap  8478  lemul12b  8643  zdivadd  9164  zdivmul  9165  elfz  9827  fzmmmeqm  9869  fzrev  9895  absdiflt  10896  absdifle  10897  dvds0lem  11539  dvdsmulc  11557  dvds2add  11563  dvds2sub  11564  dvdstr  11566  lcmdvds  11796  psmettri2  12536  xmettri2  12569