Theorem 3coml 1133

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  spc3egv  3548  omwordri  8504  oeword  8523  f1oen2g  8912  f1dom2g  8913  f1imaenfi  9126  ordiso  9428  en3lplem2  9532  axdc3lem4  10373  ltasr  11021  adddir  11133  axltadd  11217  pnpcan2  11432  subdir  11582  ltaddsub  11622  leaddsub  11624  mulcan2g  11802  div13  11828  ltdiv2  12040  lediv2  12044  zdiv  12597  xadddir  13246  xadddi2r  13248  fzen  13493  fzrevral2  13565  fzshftral  13567  ssfzoulel  13713  fzind2  13741  flflp1  13764  mulbinom2  14183  digit1  14197  faclbnd5  14258  ccatlcan  14678  elicc4abs  15280  dvdsnegb  16240  muldvds1  16247  muldvds2  16248  dvdscmul  16249  dvdsmulc  16250  dvdscmulr  16251  dvdsmulcr  16252  dvdsgcd  16511  mulgcdr  16517  lcmgcdeq  16579  congr  16631  mulgnnass  19083  gaass  19270  elfm3  23940  mettri  24342  cnmet  24761  addcnlem  24855  bcthlem5  25320  isppw2  27103  vmappw  27104  bcmono  27265  lestr  27751  ltadds1im  28002  colinearalg  29004  ax5seglem1  29022  ax5seglem2  29023  vcdir  30662  vcass  30663  imsmetlem  30786  hvaddcan2  31167  hvsubcan2  31171  dfgcd3  37691  isbasisrelowllem1  37724  ltflcei  37982  fzmul  38115  brcnvrabga  38716  pclfinclN  40449  rabrenfdioph  43266  uun123p2  45260  isosctrlem1ALT  45384