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  6644  f1oen2g  6914  f1dom2g  6915  ordiso  7211  addassnqg  7577  ltbtwnnqq  7610  nnanq0  7653  ltasrg  7965  recexgt0sr  7968  axmulass  8068  adddir  8145  axltadd  8224  ltleletr  8236  letr  8237  pnpcan2  8394  subdir  8540  div13ap  8848  zdiv  9543  xrletr  10012  fzen  10247  fzrevral2  10310  fzshftral  10312  fzind2  10453  mulbinom2  10886  ccatlcan  11258  elicc4abs  11613  dvdsnegb  12327  muldvds1  12335  muldvds2  12336  dvdscmul  12337  dvdsmulc  12338  dvdsgcd  12541  mulgcdr  12547  lcmgcdeq  12613  congr  12630  mulgnnass  13702  mettri  15055  cnmet  15212  addcncntoplem  15243