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  3557  omwordri  8583  oeword  8602  f1oen2g  8998  f1dom2g  8999  f1imaenfi  9213  ordiso  9513  en3lplem2  9617  axdc3lem4  10534  ltasr  11188  adddir  11300  axltadd  11386  pnpcan2  11601  subdir  11753  ltaddsub  11793  leaddsub  11795  mulcan2g  11973  div13  11998  ltdiv2  12206  lediv2  12210  zdiv  12772  xadddir  13429  xadddi2r  13431  fzen  13677  fzrevral2  13750  fzshftral  13752  ssfzoulel  13898  fzind2  13926  flflp1  13950  mulbinom2  14370  digit1  14384  faclbnd5  14445  ccatlcan  14871  elicc4abs  15492  dvdsnegb  16448  muldvds1  16455  muldvds2  16456  dvdscmul  16457  dvdsmulc  16458  dvdscmulr  16459  dvdsmulcr  16460  dvdsgcd  16722  mulgcdr  16728  lcmgcdeq  16792  congr  16844  mulgnnass  19324  gaass  19516  elfm3  24274  mettri  24676  cnmet  25095  addcnlem  25189  bcthlem5  25654  isppw2  27447  vmappw  27448  bcmono  27609  lestr  28124  ltadds1im  28376  colinearalg  29493  ax5seglem1  29511  ax5seglem2  29512  vcdir  31173  vcass  31174  imsmetlem  31297  hvaddcan2  31678  hvsubcan2  31682  nmulle  37058  naddle  37060  dfgcd3  38338  isbasisrelowllem1  38371  ltflcei  38624  fzmul  38768  brcnvrabga  39367  pclfinclN  41100  rabrenfdioph  43914  uun123p2  45885  isosctrlem1ALT  46009