Theorem 3coml 1189

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

Syntax hints:   → wi 4   ∧ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  3comr  1190  nndir  6394  f1oen2g  6657  f1dom2g  6658  ordiso  6929  addassnqg  7214  ltbtwnnqq  7247  nnanq0  7290  ltasrg  7602  recexgt0sr  7605  axmulass  7705  adddir  7781  axltadd  7858  ltleletr  7870  letr  7871  pnpcan2  8026  subdir  8172  div13ap  8477  zdiv  9163  xrletr  9621  fzen  9854  fzrevral2  9917  fzshftral  9919  fzind2  10047  mulbinom2  10439  elicc4abs  10898  dvdsnegb  11546  muldvds1  11554  muldvds2  11555  dvdscmul  11556  dvdsmulc  11557  dvdsgcd  11736  mulgcdr  11742  lcmgcdeq  11800  congr  11817  mettri  12581  cnmet  12738  addcncntoplem  12759