Theorem 3coml 1241

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

Syntax hints:   → wi 4   ∧ w3a 1009

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 1011

This theorem is referenced by:  3comr  1242  nndir  6757  f1oen2g  7035  f1dom2g  7036  ordiso  7370  addassnqg  7743  ltbtwnnqq  7776  nnanq0  7819  ltasrg  8131  recexgt0sr  8134  axmulass  8234  adddir  8311  axltadd  8389  ltleletr  8401  letr  8402  pnpcan2  8560  subdir  8707  div13ap  9017  zdiv  9717  xrletr  10193  fzen  10430  fzrevral2  10496  fzshftral  10498  fzind2  10641  mulbinom2  11076  ccatlcan  11473  elicc4abs  11843  dvdsnegb  12558  muldvds1  12566  muldvds2  12567  dvdscmul  12568  dvdsmulc  12569  dvdsgcd  12772  mulgcdr  12778  lcmgcdeq  12844  congr  12861  mulgnnass  13943  mettri  15457  cnmet  15614  addcncntoplem  15645