Theorem 3coml 1212

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  3comr  1213  nndir  6557  f1oen2g  6823  f1dom2g  6824  ordiso  7111  addassnqg  7468  ltbtwnnqq  7501  nnanq0  7544  ltasrg  7856  recexgt0sr  7859  axmulass  7959  adddir  8036  axltadd  8115  ltleletr  8127  letr  8128  pnpcan2  8285  subdir  8431  div13ap  8739  zdiv  9433  xrletr  9902  fzen  10137  fzrevral2  10200  fzshftral  10202  fzind2  10334  mulbinom2  10767  elicc4abs  11278  dvdsnegb  11992  muldvds1  12000  muldvds2  12001  dvdscmul  12002  dvdsmulc  12003  dvdsgcd  12206  mulgcdr  12212  lcmgcdeq  12278  congr  12295  mulgnnass  13365  mettri  14717  cnmet  14874  addcncntoplem  14905