Theorem 3coml 1210

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  3comr  1211  nndir  6490  f1oen2g  6754  f1dom2g  6755  ordiso  7034  addassnqg  7380  ltbtwnnqq  7413  nnanq0  7456  ltasrg  7768  recexgt0sr  7771  axmulass  7871  adddir  7947  axltadd  8026  ltleletr  8038  letr  8039  pnpcan2  8196  subdir  8342  div13ap  8649  zdiv  9340  xrletr  9807  fzen  10042  fzrevral2  10105  fzshftral  10107  fzind2  10238  mulbinom2  10636  elicc4abs  11102  dvdsnegb  11814  muldvds1  11822  muldvds2  11823  dvdscmul  11824  dvdsmulc  11825  dvdsgcd  12012  mulgcdr  12018  lcmgcdeq  12082  congr  12099  mulgnnass  13016  mettri  13843  cnmet  14000  addcncntoplem  14021