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 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  spc3egv  3594  omwordri  8569  oeword  8587  f1oen2g  8961  f1dom2g  8962  f1dom2gOLD  8963  f1imaenfi  9195  ordiso  9508  en3lplem2  9605  axdc3lem4  10445  ltasr  11092  adddir  11202  axltadd  11284  pnpcan2  11497  subdir  11645  ltaddsub  11685  leaddsub  11687  mulcan2g  11865  div13  11890  ltdiv2  12097  lediv2  12101  zdiv  12629  xadddir  13272  xadddi2r  13274  fzen  13515  fzrevral2  13584  fzshftral  13586  ssfzoulel  13723  fzind2  13747  flflp1  13769  mulbinom2  14183  digit1  14197  faclbnd5  14255  ccatlcan  14665  elicc4abs  15263  dvdsnegb  16214  muldvds1  16221  muldvds2  16222  dvdscmul  16223  dvdsmulc  16224  dvdscmulr  16225  dvdsmulcr  16226  dvdsgcd  16483  mulgcdr  16489  lcmgcdeq  16546  congr  16598  mulgnnass  18984  gaass  19156  elfm3  23446  mettri  23850  cnmet  24280  addcnlem  24372  bcthlem5  24837  isppw2  26609  vmappw  26610  bcmono  26770  sletr  27251  sltadd1im  27458  colinearalg  28158  ax5seglem1  28176  ax5seglem2  28177  vcdir  29807  vcass  29808  imsmetlem  29931  hvaddcan2  30312  hvsubcan2  30316  dfgcd3  36194  isbasisrelowllem1  36225  ltflcei  36465  fzmul  36598  brcnvrabga  37200  pclfinclN  38810  rabrenfdioph  41538  uun123p2  43557  isosctrlem1ALT  43681