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  3565  omwordri  8566  oeword  8585  f1oen2g  8974  f1dom2g  8975  f1imaenfi  9189  ordiso  9488  en3lplem2  9592  axdc3lem4  10455  ltasr  11103  adddir  11215  axltadd  11301  pnpcan2  11516  subdir  11666  ltaddsub  11706  leaddsub  11708  mulcan2g  11886  div13  11911  ltdiv2  12119  lediv2  12123  zdiv  12684  xadddir  13340  xadddi2r  13342  fzen  13587  fzrevral2  13660  fzshftral  13662  ssfzoulel  13808  fzind2  13836  flflp1  13860  mulbinom2  14279  digit1  14293  faclbnd5  14354  ccatlcan  14779  elicc4abs  15397  dvdsnegb  16356  muldvds1  16363  muldvds2  16364  dvdscmul  16365  dvdsmulc  16366  dvdscmulr  16367  dvdsmulcr  16368  dvdsgcd  16627  mulgcdr  16633  lcmgcdeq  16695  congr  16747  mulgnnass  19206  gaass  19398  elfm3  24144  mettri  24546  cnmet  24965  addcnlem  25059  bcthlem5  25524  isppw2  27316  vmappw  27317  bcmono  27478  lestr  27963  ltadds1im  28215  colinearalg  29297  ax5seglem1  29315  ax5seglem2  29316  vcdir  30955  vcass  30956  imsmetlem  31079  hvaddcan2  31460  hvsubcan2  31464  nmulle  36730  naddle  36732  dfgcd3  38009  isbasisrelowllem1  38042  ltflcei  38300  fzmul  38433  brcnvrabga  39032  pclfinclN  40765  rabrenfdioph  43582  uun123p2  45559  isosctrlem1ALT  45683