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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  spc3egv  3560  omwordri  8563  oeword  8582  f1oen2g  8978  f1dom2g  8979  f1imaenfi  9193  ordiso  9492  en3lplem2  9596  axdc3lem4  10459  ltasr  11113  adddir  11225  axltadd  11311  pnpcan2  11526  subdir  11676  ltaddsub  11716  leaddsub  11718  mulcan2g  11896  div13  11921  ltdiv2  12129  lediv2  12133  zdiv  12695  xadddir  13352  xadddi2r  13354  fzen  13599  fzrevral2  13672  fzshftral  13674  ssfzoulel  13820  fzind2  13848  flflp1  13872  mulbinom2  14291  digit1  14305  faclbnd5  14366  ccatlcan  14791  elicc4abs  15411  dvdsnegb  16369  muldvds1  16376  muldvds2  16377  dvdscmul  16378  dvdsmulc  16379  dvdscmulr  16380  dvdsmulcr  16381  dvdsgcd  16640  mulgcdr  16646  lcmgcdeq  16708  congr  16760  mulgnnass  19238  gaass  19430  elfm3  24182  mettri  24584  cnmet  25003  addcnlem  25097  bcthlem5  25562  isppw2  27359  vmappw  27360  bcmono  27521  lestr  28006  ltadds1im  28258  colinearalg  29375  ax5seglem1  29393  ax5seglem2  29394  vcdir  31055  vcass  31056  imsmetlem  31179  hvaddcan2  31560  hvsubcan2  31564  nmulle  36805  naddle  36807  dfgcd3  38084  isbasisrelowllem1  38117  ltflcei  38370  fzmul  38499  brcnvrabga  39098  pclfinclN  40831  rabrenfdioph  43663  uun123p2  45640  isosctrlem1ALT  45764