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  6767  f1oen2g  7046  f1dom2g  7047  ordiso  7383  addassnqg  7756  ltbtwnnqq  7789  nnanq0  7832  ltasrg  8144  recexgt0sr  8147  axmulass  8247  adddir  8324  axltadd  8402  ltleletr  8414  letr  8415  pnpcan2  8574  subdir  8721  div13ap  9032  zdiv  9746  xrletr  10228  fzen  10465  fzrevral2  10531  fzshftral  10533  fzind2  10676  mulbinom2  11115  ccatlcan  11513  elicc4abs  11884  dvdsnegb  12601  muldvds1  12609  muldvds2  12610  dvdscmul  12611  dvdsmulc  12612  dvdsgcd  12815  mulgcdr  12821  lcmgcdeq  12887  congr  12904  mulgnnass  14020  mettri  15611  cnmet  15768  addcncntoplem  15799  bcmono  16316