Theorem 3coml 1145

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

Syntax hints:   → wi 4   ∧ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  3comr  1146  nndir  6092  f1oen2g  6258  f1dom2g  6259  ordiso  6447  addassnqg  6572  ltbtwnnqq  6605  nnanq0  6648  ltasrg  6947  recexgt0sr  6950  axmulass  7039  adddir  7110  axltadd  7182  ltleletr  7193  letr  7194  pnpcan2  7348  subdir  7490  div13ap  7781  zdiv  8435  xrletr  8878  fzen  9062  fzrevral2  9123  fzshftral  9125  fzind2  9248  mulbinom2  9589  elicc4abs  9980  dvdsnegb  10212  muldvds1  10220  muldvds2  10221  dvdscmul  10222  dvdsmulc  10223  dvdsgcd  10401  mulgcdr  10407  lcmgcdeq  10465  congr  10482