Theorem 3coml 1234

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  3comr  1235  nndir  6649  f1oen2g  6919  f1dom2g  6920  ordiso  7219  addassnqg  7585  ltbtwnnqq  7618  nnanq0  7661  ltasrg  7973  recexgt0sr  7976  axmulass  8076  adddir  8153  axltadd  8232  ltleletr  8244  letr  8245  pnpcan2  8402  subdir  8548  div13ap  8856  zdiv  9551  xrletr  10021  fzen  10256  fzrevral2  10319  fzshftral  10321  fzind2  10462  mulbinom2  10895  ccatlcan  11271  elicc4abs  11626  dvdsnegb  12340  muldvds1  12348  muldvds2  12349  dvdscmul  12350  dvdsmulc  12351  dvdsgcd  12554  mulgcdr  12560  lcmgcdeq  12626  congr  12643  mulgnnass  13715  mettri  15068  cnmet  15225  addcncntoplem  15256