Theorem 3coml 1213

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  3comr  1214  nndir  6586  f1oen2g  6856  f1dom2g  6857  ordiso  7150  addassnqg  7508  ltbtwnnqq  7541  nnanq0  7584  ltasrg  7896  recexgt0sr  7899  axmulass  7999  adddir  8076  axltadd  8155  ltleletr  8167  letr  8168  pnpcan2  8325  subdir  8471  div13ap  8779  zdiv  9474  xrletr  9943  fzen  10178  fzrevral2  10241  fzshftral  10243  fzind2  10381  mulbinom2  10814  elicc4abs  11455  dvdsnegb  12169  muldvds1  12177  muldvds2  12178  dvdscmul  12179  dvdsmulc  12180  dvdsgcd  12383  mulgcdr  12389  lcmgcdeq  12455  congr  12472  mulgnnass  13543  mettri  14895  cnmet  15052  addcncntoplem  15083