Theorem 3coml 1236

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  3comr  1237  nndir  6658  f1oen2g  6928  f1dom2g  6929  ordiso  7235  addassnqg  7602  ltbtwnnqq  7635  nnanq0  7678  ltasrg  7990  recexgt0sr  7993  axmulass  8093  adddir  8170  axltadd  8249  ltleletr  8261  letr  8262  pnpcan2  8419  subdir  8565  div13ap  8873  zdiv  9568  xrletr  10043  fzen  10278  fzrevral2  10341  fzshftral  10343  fzind2  10486  mulbinom2  10919  ccatlcan  11303  elicc4abs  11659  dvdsnegb  12374  muldvds1  12382  muldvds2  12383  dvdscmul  12384  dvdsmulc  12385  dvdsgcd  12588  mulgcdr  12594  lcmgcdeq  12660  congr  12677  mulgnnass  13749  mettri  15103  cnmet  15260  addcncntoplem  15291