Theorem 3coml 1241

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

Hypothesis

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

Assertion

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

Proof of Theorem 3coml

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3com23 1240	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)
3	2	3com13 1239	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3comr  1242  nndir  6763  f1oen2g  7041  f1dom2g  7042  ordiso  7376  addassnqg  7749  ltbtwnnqq  7782  nnanq0  7825  ltasrg  8137  recexgt0sr  8140  axmulass  8240  adddir  8317  axltadd  8395  ltleletr  8407  letr  8408  pnpcan2  8566  subdir  8713  div13ap  9024  zdiv  9736  xrletr  10212  fzen  10449  fzrevral2  10515  fzshftral  10517  fzind2  10660  mulbinom2  11095  ccatlcan  11492  elicc4abs  11862  dvdsnegb  12577  muldvds1  12585  muldvds2  12586  dvdscmul  12587  dvdsmulc  12588  dvdsgcd  12791  mulgcdr  12797  lcmgcdeq  12863  congr  12880  mulgnnass  13962  mettri  15476  cnmet  15633  addcncntoplem  15664  bcmono  16124