Theorem 3coml 1263

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

Syntax hints:   → wi 4   ∧ w3a 1030

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 195  df-an 384  df-3an 1032

This theorem is referenced by:  3comr  1264  omwordri  7517  oeword  7535  f1oen2g  7836  f1dom2g  7837  ordiso  8282  en3lplem2  8373  axdc3lem4  9136  ltasr  9778  adddir  9888  axltadd  9963  pnpcan2  10173  subdir  10316  ltaddsub  10354  leaddsub  10356  mulcan2g  10533  div13  10558  ltdiv2  10761  lediv2  10765  zdiv  11282  xadddir  11958  xadddi2r  11960  fzen  12187  fzrevral2  12253  fzshftral  12255  ssfzoulel  12386  fzind2  12406  flflp1  12428  mulbinom2  12804  digit1  12818  faclbnd5  12905  ccatlcan  13273  relexpreld  13577  elicc4abs  13856  dvdsnegb  14786  muldvds1  14793  muldvds2  14794  dvdscmul  14795  dvdsmulc  14796  dvdscmulr  14797  dvdsmulcr  14798  dvdsgcd  15048  mulgcdr  15054  lcmgcdeq  15112  coprmdvdsOLD  15154  congr  15165  mulgnnass  17348  mulgnnassOLD  17349  gaass  17502  elfm3  21512  mettri  21915  cnmet  22333  addcnlem  22423  bcthlem5  22878  isppw2  24586  vmappw  24587  bcmono  24747  colinearalg  25536  ax5seglem1  25554  ax5seglem2  25555  vcdir  26602  vcass  26603  imsmetlem  26754  hvaddcan2  27146  hvsubcan2  27150  isbasisrelowllem1  32203  ltflcei  32391  fzmul  32531  pclfinclN  34078  rabrenfdioph  36220  uun123p2  37882  isosctrlem1ALT  38016