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 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  spc3egv  3594  omwordri  8572  oeword  8590  f1oen2g  8964  f1dom2g  8965  f1dom2gOLD  8966  f1imaenfi  9198  ordiso  9511  en3lplem2  9608  axdc3lem4  10448  ltasr  11095  adddir  11205  axltadd  11287  pnpcan2  11500  subdir  11648  ltaddsub  11688  leaddsub  11690  mulcan2g  11868  div13  11893  ltdiv2  12100  lediv2  12104  zdiv  12632  xadddir  13275  xadddi2r  13277  fzen  13518  fzrevral2  13587  fzshftral  13589  ssfzoulel  13726  fzind2  13750  flflp1  13772  mulbinom2  14186  digit1  14200  faclbnd5  14258  ccatlcan  14668  elicc4abs  15266  dvdsnegb  16217  muldvds1  16224  muldvds2  16225  dvdscmul  16226  dvdsmulc  16227  dvdscmulr  16228  dvdsmulcr  16229  dvdsgcd  16486  mulgcdr  16492  lcmgcdeq  16549  congr  16601  mulgnnass  18989  gaass  19161  elfm3  23454  mettri  23858  cnmet  24288  addcnlem  24380  bcthlem5  24845  isppw2  26619  vmappw  26620  bcmono  26780  sletr  27261  sltadd1im  27468  colinearalg  28168  ax5seglem1  28186  ax5seglem2  28187  vcdir  29819  vcass  29820  imsmetlem  29943  hvaddcan2  30324  hvsubcan2  30328  dfgcd3  36205  isbasisrelowllem1  36236  ltflcei  36476  fzmul  36609  brcnvrabga  37211  pclfinclN  38821  rabrenfdioph  41552  uun123p2  43571  isosctrlem1ALT  43695