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  3558  omwordri  8487  oeword  8505  f1oen2g  8891  f1dom2g  8892  f1imaenfi  9104  ordiso  9402  en3lplem2  9503  axdc3lem4  10341  ltasr  10988  adddir  11100  axltadd  11183  pnpcan2  11398  subdir  11548  ltaddsub  11588  leaddsub  11590  mulcan2g  11768  div13  11794  ltdiv2  12005  lediv2  12009  zdiv  12540  xadddir  13192  xadddi2r  13194  fzen  13438  fzrevral2  13510  fzshftral  13512  ssfzoulel  13657  fzind2  13685  flflp1  13708  mulbinom2  14127  digit1  14141  faclbnd5  14202  ccatlcan  14622  elicc4abs  15224  dvdsnegb  16181  muldvds1  16188  muldvds2  16189  dvdscmul  16190  dvdsmulc  16191  dvdscmulr  16192  dvdsmulcr  16193  dvdsgcd  16452  mulgcdr  16458  lcmgcdeq  16520  congr  16572  mulgnnass  19019  gaass  19207  elfm3  23863  mettri  24265  cnmet  24684  addcnlem  24778  bcthlem5  25253  isppw2  27050  vmappw  27051  bcmono  27213  sletr  27695  sltadd1im  27926  colinearalg  28886  ax5seglem1  28904  ax5seglem2  28905  vcdir  30541  vcass  30542  imsmetlem  30665  hvaddcan2  31046  hvsubcan2  31050  dfgcd3  37357  isbasisrelowllem1  37388  ltflcei  37647  fzmul  37780  brcnvrabga  38369  pclfinclN  39988  rabrenfdioph  42846  uun123p2  44841  isosctrlem1ALT  44965