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  6736  f1oen2g  7007  f1dom2g  7008  ordiso  7340  addassnqg  7713  ltbtwnnqq  7746  nnanq0  7789  ltasrg  8101  recexgt0sr  8104  axmulass  8204  adddir  8281  axltadd  8359  ltleletr  8371  letr  8372  pnpcan2  8529  subdir  8676  div13ap  8984  zdiv  9684  xrletr  10160  fzen  10397  fzrevral2  10462  fzshftral  10464  fzind2  10607  mulbinom2  11042  ccatlcan  11435  elicc4abs  11804  dvdsnegb  12519  muldvds1  12527  muldvds2  12528  dvdscmul  12529  dvdsmulc  12530  dvdsgcd  12733  mulgcdr  12739  lcmgcdeq  12805  congr  12822  mulgnnass  13958  mettri  15350  cnmet  15507  addcncntoplem  15538