Theorem 3coml 1237

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  3comr  1238  nndir  6701  f1oen2g  6971  f1dom2g  6972  ordiso  7278  addassnqg  7645  ltbtwnnqq  7678  nnanq0  7721  ltasrg  8033  recexgt0sr  8036  axmulass  8136  adddir  8213  axltadd  8292  ltleletr  8304  letr  8305  pnpcan2  8462  subdir  8608  div13ap  8916  zdiv  9611  xrletr  10086  fzen  10321  fzrevral2  10384  fzshftral  10386  fzind2  10529  mulbinom2  10962  ccatlcan  11346  elicc4abs  11715  dvdsnegb  12430  muldvds1  12438  muldvds2  12439  dvdscmul  12440  dvdsmulc  12441  dvdsgcd  12644  mulgcdr  12650  lcmgcdeq  12716  congr  12733  mulgnnass  13805  mettri  15164  cnmet  15321  addcncntoplem  15352