Theorem 3comr 1235

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  nnacan  6675  le2tri3i  8278  ltaddsublt  8741  div12ap  8864  lemul12b  9031  zdivadd  9559  zdivmul  9560  elfz  10239  fzmmmeqm  10283  fzrev  10309  absdiflt  11643  absdifle  11644  dvds0lem  12352  dvdsmulc  12370  dvds2add  12376  dvds2sub  12377  dvdstr  12379  lcmdvds  12641  psmettri2  15042  xmettri2  15075