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 1142	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  spc3egv  3563  omwordri  8558  oeword  8577  f1oen2g  8966  f1dom2g  8967  f1imaenfi  9180  ordiso  9479  en3lplem2  9583  axdc3lem4  10438  ltasr  11086  adddir  11198  axltadd  11284  pnpcan2  11499  subdir  11649  ltaddsub  11689  leaddsub  11691  mulcan2g  11869  div13  11894  ltdiv2  12102  lediv2  12106  zdiv  12667  xadddir  13323  xadddi2r  13325  fzen  13570  fzrevral2  13643  fzshftral  13645  ssfzoulel  13791  fzind2  13819  flflp1  13842  mulbinom2  14261  digit1  14275  faclbnd5  14336  ccatlcan  14757  elicc4abs  15373  dvdsnegb  16332  muldvds1  16339  muldvds2  16340  dvdscmul  16341  dvdsmulc  16342  dvdscmulr  16343  dvdsmulcr  16344  dvdsgcd  16603  mulgcdr  16609  lcmgcdeq  16671  congr  16723  mulgnnass  19176  gaass  19368  elfm3  24088  mettri  24490  cnmet  24909  addcnlem  25003  bcthlem5  25468  isppw2  27260  vmappw  27261  bcmono  27422  lestr  27907  ltadds1im  28159  colinearalg  29241  ax5seglem1  29259  ax5seglem2  29260  vcdir  30899  vcass  30900  imsmetlem  31023  hvaddcan2  31404  hvsubcan2  31408  nmulle  36675  naddle  36677  dfgcd3  37949  isbasisrelowllem1  37982  ltflcei  38240  fzmul  38373  brcnvrabga  38972  pclfinclN  40705  rabrenfdioph  43524  uun123p2  45501  isosctrlem1ALT  45625