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  6493  f1oen2g  6757  f1dom2g  6758  ordiso  7037  addassnqg  7383  ltbtwnnqq  7416  nnanq0  7459  ltasrg  7771  recexgt0sr  7774  axmulass  7874  adddir  7950  axltadd  8029  ltleletr  8041  letr  8042  pnpcan2  8199  subdir  8345  div13ap  8652  zdiv  9343  xrletr  9810  fzen  10045  fzrevral2  10108  fzshftral  10110  fzind2  10241  mulbinom2  10639  elicc4abs  11105  dvdsnegb  11817  muldvds1  11825  muldvds2  11826  dvdscmul  11827  dvdsmulc  11828  dvdsgcd  12015  mulgcdr  12021  lcmgcdeq  12085  congr  12102  mulgnnass  13023  mettri  13912  cnmet  14069  addcncntoplem  14090