Theorem 3coml 1127

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 1126	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)
3	2	3com13 1124	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  spc3egv  3557  omwordri  8499  oeword  8518  f1oen2g  8905  f1dom2g  8906  f1imaenfi  9119  ordiso  9421  en3lplem2  9522  axdc3lem4  10363  ltasr  11011  adddir  11123  axltadd  11206  pnpcan2  11421  subdir  11571  ltaddsub  11611  leaddsub  11613  mulcan2g  11791  div13  11817  ltdiv2  12028  lediv2  12032  zdiv  12562  xadddir  13211  xadddi2r  13213  fzen  13457  fzrevral2  13529  fzshftral  13531  ssfzoulel  13676  fzind2  13704  flflp1  13727  mulbinom2  14146  digit1  14160  faclbnd5  14221  ccatlcan  14641  elicc4abs  15243  dvdsnegb  16200  muldvds1  16207  muldvds2  16208  dvdscmul  16209  dvdsmulc  16210  dvdscmulr  16211  dvdsmulcr  16212  dvdsgcd  16471  mulgcdr  16477  lcmgcdeq  16539  congr  16591  mulgnnass  19039  gaass  19226  elfm3  23894  mettri  24296  cnmet  24715  addcnlem  24809  bcthlem5  25284  isppw2  27081  vmappw  27082  bcmono  27244  lestr  27730  ltadds1im  27981  colinearalg  28983  ax5seglem1  29001  ax5seglem2  29002  vcdir  30641  vcass  30642  imsmetlem  30765  hvaddcan2  31146  hvsubcan2  31150  dfgcd3  37525  isbasisrelowllem1  37556  ltflcei  37805  fzmul  37938  brcnvrabga  38531  pclfinclN  40206  rabrenfdioph  43052  uun123p2  45046  isosctrlem1ALT  45170