Theorem 3coml 1241

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3comr  1242  nndir  6763  f1oen2g  7041  f1dom2g  7042  ordiso  7377  addassnqg  7750  ltbtwnnqq  7783  nnanq0  7826  ltasrg  8138  recexgt0sr  8141  axmulass  8241  adddir  8318  axltadd  8396  ltleletr  8408  letr  8409  pnpcan2  8568  subdir  8715  div13ap  9026  zdiv  9739  xrletr  10221  fzen  10458  fzrevral2  10524  fzshftral  10526  fzind2  10669  mulbinom2  11107  ccatlcan  11505  elicc4abs  11876  dvdsnegb  12593  muldvds1  12601  muldvds2  12602  dvdscmul  12603  dvdsmulc  12604  dvdsgcd  12807  mulgcdr  12813  lcmgcdeq  12879  congr  12896  mulgnnass  14011  mettri  15526  cnmet  15683  addcncntoplem  15714  bcmono  16226