Theorem 3coml 1139

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  spc3egv  3562  omwordri  8536  oeword  8555  f1oen2g  8945  f1dom2g  8946  f1imaenfi  9159  ordiso  9461  en3lplem2  9565  axdc3lem4  10407  ltasr  11055  adddir  11167  axltadd  11253  pnpcan2  11468  subdir  11618  ltaddsub  11658  leaddsub  11660  mulcan2g  11838  div13  11863  ltdiv2  12075  lediv2  12079  zdiv  12640  xadddir  13296  xadddi2r  13298  fzen  13543  fzrevral2  13615  fzshftral  13617  ssfzoulel  13763  fzind2  13791  flflp1  13814  mulbinom2  14233  digit1  14247  faclbnd5  14308  ccatlcan  14728  elicc4abs  15330  dvdsnegb  16290  muldvds1  16297  muldvds2  16298  dvdscmul  16299  dvdsmulc  16300  dvdscmulr  16301  dvdsmulcr  16302  dvdsgcd  16561  mulgcdr  16567  lcmgcdeq  16629  congr  16681  mulgnnass  19134  gaass  19320  elfm3  23990  mettri  24392  cnmet  24811  addcnlem  24905  bcthlem5  25370  isppw2  27156  vmappw  27157  bcmono  27318  lestr  27803  ltadds1im  28055  colinearalg  29057  ax5seglem1  29075  ax5seglem2  29076  vcdir  30715  vcass  30716  imsmetlem  30839  hvaddcan2  31220  hvsubcan2  31224  dfgcd3  37780  isbasisrelowllem1  37813  ltflcei  38071  fzmul  38204  brcnvrabga  38805  pclfinclN  40538  rabrenfdioph  43355  uun123p2  45349  isosctrlem1ALT  45473