Theorem 3coml 1156

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

Syntax hints:   → wi 4   ∧ w3a 930

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

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

This theorem is referenced by:  3comr  1157  nndir  6316  f1oen2g  6579  f1dom2g  6580  ordiso  6836  addassnqg  7091  ltbtwnnqq  7124  nnanq0  7167  ltasrg  7466  recexgt0sr  7469  axmulass  7558  adddir  7629  axltadd  7706  ltleletr  7717  letr  7718  pnpcan2  7873  subdir  8015  div13ap  8314  zdiv  8991  xrletr  9432  fzen  9664  fzrevral2  9727  fzshftral  9729  fzind2  9857  mulbinom2  10249  elicc4abs  10706  dvdsnegb  11305  muldvds1  11313  muldvds2  11314  dvdscmul  11315  dvdsmulc  11316  dvdsgcd  11493  mulgcdr  11499  lcmgcdeq  11557  congr  11574  mettri  12301  cnmet  12452