Theorem 3coml 1212

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  3comr  1213  nndir  6515  f1oen2g  6781  f1dom2g  6782  ordiso  7065  addassnqg  7411  ltbtwnnqq  7444  nnanq0  7487  ltasrg  7799  recexgt0sr  7802  axmulass  7902  adddir  7978  axltadd  8057  ltleletr  8069  letr  8070  pnpcan2  8227  subdir  8373  div13ap  8680  zdiv  9371  xrletr  9838  fzen  10073  fzrevral2  10136  fzshftral  10138  fzind2  10269  mulbinom2  10668  elicc4abs  11135  dvdsnegb  11847  muldvds1  11855  muldvds2  11856  dvdscmul  11857  dvdsmulc  11858  dvdsgcd  12045  mulgcdr  12051  lcmgcdeq  12115  congr  12132  mulgnnass  13097  mettri  14333  cnmet  14490  addcncntoplem  14511