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  6666  le2tri3i  8266  ltaddsublt  8729  div12ap  8852  lemul12b  9019  zdivadd  9547  zdivmul  9548  elfz  10222  fzmmmeqm  10266  fzrev  10292  absdiflt  11618  absdifle  11619  dvds0lem  12327  dvdsmulc  12345  dvds2add  12351  dvds2sub  12352  dvdstr  12354  lcmdvds  12616  psmettri2  15017  xmettri2  15050