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  6722  f1oen2g  6993  f1dom2g  6994  ordiso  7326  addassnqg  7696  ltbtwnnqq  7729  nnanq0  7772  ltasrg  8084  recexgt0sr  8087  axmulass  8187  adddir  8264  axltadd  8342  ltleletr  8354  letr  8355  pnpcan2  8512  subdir  8658  div13ap  8966  zdiv  9665  xrletr  10140  fzen  10376  fzrevral2  10439  fzshftral  10441  fzind2  10584  mulbinom2  11017  ccatlcan  11406  elicc4abs  11775  dvdsnegb  12490  muldvds1  12498  muldvds2  12499  dvdscmul  12500  dvdsmulc  12501  dvdsgcd  12704  mulgcdr  12710  lcmgcdeq  12776  congr  12793  mulgnnass  13866  mettri  15230  cnmet  15387  addcncntoplem  15418