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 1087

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 1089

This theorem is referenced by:  spc3egv  3545  omwordri  8507  oeword  8526  f1oen2g  8915  f1dom2g  8916  f1imaenfi  9129  ordiso  9431  en3lplem2  9534  axdc3lem4  10375  ltasr  11023  adddir  11135  axltadd  11219  pnpcan2  11434  subdir  11584  ltaddsub  11624  leaddsub  11626  mulcan2g  11804  div13  11830  ltdiv2  12042  lediv2  12046  zdiv  12599  xadddir  13248  xadddi2r  13250  fzen  13495  fzrevral2  13567  fzshftral  13569  ssfzoulel  13715  fzind2  13743  flflp1  13766  mulbinom2  14185  digit1  14199  faclbnd5  14260  ccatlcan  14680  elicc4abs  15282  dvdsnegb  16242  muldvds1  16249  muldvds2  16250  dvdscmul  16251  dvdsmulc  16252  dvdscmulr  16253  dvdsmulcr  16254  dvdsgcd  16513  mulgcdr  16519  lcmgcdeq  16581  congr  16633  mulgnnass  19085  gaass  19272  elfm3  23915  mettri  24317  cnmet  24736  addcnlem  24830  bcthlem5  25295  isppw2  27078  vmappw  27079  bcmono  27240  lestr  27726  ltadds1im  27977  colinearalg  28979  ax5seglem1  28997  ax5seglem2  28998  vcdir  30637  vcass  30638  imsmetlem  30761  hvaddcan2  31142  hvsubcan2  31146  dfgcd3  37638  isbasisrelowllem1  37671  ltflcei  37929  fzmul  38062  brcnvrabga  38663  pclfinclN  40396  rabrenfdioph  43242  uun123p2  45236  isosctrlem1ALT  45360