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  6725  f1oen2g  6996  f1dom2g  6997  ordiso  7329  addassnqg  7699  ltbtwnnqq  7732  nnanq0  7775  ltasrg  8087  recexgt0sr  8090  axmulass  8190  adddir  8267  axltadd  8345  ltleletr  8357  letr  8358  pnpcan2  8515  subdir  8661  div13ap  8969  zdiv  9669  xrletr  10144  fzen  10380  fzrevral2  10444  fzshftral  10446  fzind2  10589  mulbinom2  11022  ccatlcan  11414  elicc4abs  11783  dvdsnegb  12498  muldvds1  12506  muldvds2  12507  dvdscmul  12508  dvdsmulc  12509  dvdsgcd  12712  mulgcdr  12718  lcmgcdeq  12784  congr  12801  mulgnnass  13891  mettri  15255  cnmet  15412  addcncntoplem  15443