Theorem 3coml 1145

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  spc3egv  3558  omwordri  8564  oeword  8583  f1oen2g  8979  f1dom2g  8980  f1imaenfi  9194  ordiso  9494  en3lplem2  9598  axdc3lem4  10512  ltasr  11166  adddir  11278  axltadd  11364  pnpcan2  11579  subdir  11731  ltaddsub  11771  leaddsub  11773  mulcan2g  11951  div13  11976  ltdiv2  12184  lediv2  12188  zdiv  12750  xadddir  13407  xadddi2r  13409  fzen  13654  fzrevral2  13727  fzshftral  13729  ssfzoulel  13875  fzind2  13903  flflp1  13927  mulbinom2  14347  digit1  14361  faclbnd5  14422  ccatlcan  14847  elicc4abs  15467  dvdsnegb  16423  muldvds1  16430  muldvds2  16431  dvdscmul  16432  dvdsmulc  16433  dvdscmulr  16434  dvdsmulcr  16435  dvdsgcd  16697  mulgcdr  16703  lcmgcdeq  16767  congr  16819  mulgnnass  19299  gaass  19491  elfm3  24249  mettri  24651  cnmet  25070  addcnlem  25164  bcthlem5  25629  isppw2  27424  vmappw  27425  bcmono  27586  lestr  28101  ltadds1im  28353  colinearalg  29470  ax5seglem1  29488  ax5seglem2  29489  vcdir  31150  vcass  31151  imsmetlem  31274  hvaddcan2  31655  hvsubcan2  31659  nmulle  36936  naddle  36938  dfgcd3  38213  isbasisrelowllem1  38246  ltflcei  38499  fzmul  38643  brcnvrabga  39242  pclfinclN  40975  rabrenfdioph  43774  uun123p2  45751  isosctrlem1ALT  45875