Theorem 3coml 1126

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

Syntax hints:   → wi 4   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088

This theorem is referenced by:  spc3egv  3542  omwordri  8403  oeword  8421  f1oen2g  8756  f1dom2g  8757  f1dom2gOLD  8758  f1imaenfi  8981  ordiso  9275  en3lplem2  9371  axdc3lem4  10209  ltasr  10856  adddir  10966  axltadd  11048  pnpcan2  11261  subdir  11409  ltaddsub  11449  leaddsub  11451  mulcan2g  11629  div13  11654  ltdiv2  11861  lediv2  11865  zdiv  12390  xadddir  13030  xadddi2r  13032  fzen  13273  fzrevral2  13342  fzshftral  13344  ssfzoulel  13481  fzind2  13505  flflp1  13527  mulbinom2  13938  digit1  13952  faclbnd5  14012  ccatlcan  14431  elicc4abs  15031  dvdsnegb  15983  muldvds1  15990  muldvds2  15991  dvdscmul  15992  dvdsmulc  15993  dvdscmulr  15994  dvdsmulcr  15995  dvdsgcd  16252  mulgcdr  16258  lcmgcdeq  16317  congr  16369  mulgnnass  18738  gaass  18903  elfm3  23101  mettri  23505  cnmet  23935  addcnlem  24027  bcthlem5  24492  isppw2  26264  vmappw  26265  bcmono  26425  colinearalg  27278  ax5seglem1  27296  ax5seglem2  27297  vcdir  28928  vcass  28929  imsmetlem  29052  hvaddcan2  29433  hvsubcan2  29437  sletr  33961  dfgcd3  35495  isbasisrelowllem1  35526  ltflcei  35765  fzmul  35899  brcnvrabga  36477  pclfinclN  37964  rabrenfdioph  40636  uun123p2  42430  isosctrlem1ALT  42554