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  3554  omwordri  8493  oeword  8511  f1oen2g  8897  f1dom2g  8898  f1imaenfi  9111  ordiso  9409  en3lplem2  9510  axdc3lem4  10351  ltasr  10998  adddir  11110  axltadd  11193  pnpcan2  11408  subdir  11558  ltaddsub  11598  leaddsub  11600  mulcan2g  11778  div13  11804  ltdiv2  12015  lediv2  12019  zdiv  12549  xadddir  13197  xadddi2r  13199  fzen  13443  fzrevral2  13515  fzshftral  13517  ssfzoulel  13662  fzind2  13690  flflp1  13713  mulbinom2  14132  digit1  14146  faclbnd5  14207  ccatlcan  14627  elicc4abs  15229  dvdsnegb  16186  muldvds1  16193  muldvds2  16194  dvdscmul  16195  dvdsmulc  16196  dvdscmulr  16197  dvdsmulcr  16198  dvdsgcd  16457  mulgcdr  16463  lcmgcdeq  16525  congr  16577  mulgnnass  19024  gaass  19211  elfm3  23866  mettri  24268  cnmet  24687  addcnlem  24781  bcthlem5  25256  isppw2  27053  vmappw  27054  bcmono  27216  sletr  27698  sltadd1im  27929  colinearalg  28890  ax5seglem1  28908  ax5seglem2  28909  vcdir  30548  vcass  30549  imsmetlem  30672  hvaddcan2  31053  hvsubcan2  31057  dfgcd3  37389  isbasisrelowllem1  37420  ltflcei  37669  fzmul  37802  brcnvrabga  38395  pclfinclN  40070  rabrenfdioph  42932  uun123p2  44927  isosctrlem1ALT  45051