Theorem 3coml 1128

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  spc3egv  3546  omwordri  8500  oeword  8519  f1oen2g  8908  f1dom2g  8909  f1imaenfi  9122  ordiso  9424  en3lplem2  9525  axdc3lem4  10366  ltasr  11014  adddir  11126  axltadd  11210  pnpcan2  11425  subdir  11575  ltaddsub  11615  leaddsub  11617  mulcan2g  11795  div13  11821  ltdiv2  12033  lediv2  12037  zdiv  12590  xadddir  13239  xadddi2r  13241  fzen  13486  fzrevral2  13558  fzshftral  13560  ssfzoulel  13706  fzind2  13734  flflp1  13757  mulbinom2  14176  digit1  14190  faclbnd5  14251  ccatlcan  14671  elicc4abs  15273  dvdsnegb  16233  muldvds1  16240  muldvds2  16241  dvdscmul  16242  dvdsmulc  16243  dvdscmulr  16244  dvdsmulcr  16245  dvdsgcd  16504  mulgcdr  16510  lcmgcdeq  16572  congr  16624  mulgnnass  19076  gaass  19263  elfm3  23925  mettri  24327  cnmet  24746  addcnlem  24840  bcthlem5  25305  isppw2  27092  vmappw  27093  bcmono  27254  lestr  27740  ltadds1im  27991  colinearalg  28993  ax5seglem1  29011  ax5seglem2  29012  vcdir  30652  vcass  30653  imsmetlem  30776  hvaddcan2  31157  hvsubcan2  31161  dfgcd3  37654  isbasisrelowllem1  37685  ltflcei  37943  fzmul  38076  brcnvrabga  38677  pclfinclN  40410  rabrenfdioph  43260  uun123p2  45254  isosctrlem1ALT  45378