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  6653  f1oen2g  6923  f1dom2g  6924  ordiso  7229  addassnqg  7595  ltbtwnnqq  7628  nnanq0  7671  ltasrg  7983  recexgt0sr  7986  axmulass  8086  adddir  8163  axltadd  8242  ltleletr  8254  letr  8255  pnpcan2  8412  subdir  8558  div13ap  8866  zdiv  9561  xrletr  10036  fzen  10271  fzrevral2  10334  fzshftral  10336  fzind2  10478  mulbinom2  10911  ccatlcan  11292  elicc4abs  11648  dvdsnegb  12362  muldvds1  12370  muldvds2  12371  dvdscmul  12372  dvdsmulc  12373  dvdsgcd  12576  mulgcdr  12582  lcmgcdeq  12648  congr  12665  mulgnnass  13737  mettri  15090  cnmet  15247  addcncntoplem  15278