Theorem 3coml 1264

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3comr  1265  omwordri  7539  oeword  7557  f1oen2g  7858  f1dom2g  7859  ordiso  8304  en3lplem2  8395  axdc3lem4  9158  ltasr  9800  adddir  9910  axltadd  9990  pnpcan2  10200  subdir  10343  ltaddsub  10381  leaddsub  10383  mulcan2g  10560  div13  10585  ltdiv2  10788  lediv2  10792  zdiv  11323  xadddir  11998  xadddi2r  12000  fzen  12229  fzrevral2  12295  fzshftral  12297  ssfzoulel  12428  fzind2  12448  flflp1  12470  mulbinom2  12846  digit1  12860  faclbnd5  12947  ccatlcan  13324  relexpreld  13628  elicc4abs  13907  dvdsnegb  14837  muldvds1  14844  muldvds2  14845  dvdscmul  14846  dvdsmulc  14847  dvdscmulr  14848  dvdsmulcr  14849  dvdsgcd  15099  mulgcdr  15105  lcmgcdeq  15163  coprmdvdsOLD  15205  congr  15216  mulgnnass  17399  mulgnnassOLD  17400  gaass  17553  elfm3  21564  mettri  21967  cnmet  22385  addcnlem  22475  bcthlem5  22933  isppw2  24641  vmappw  24642  bcmono  24802  colinearalg  25590  ax5seglem1  25608  ax5seglem2  25609  vcdir  26805  vcass  26806  imsmetlem  26929  hvaddcan2  27312  hvsubcan2  27316  isbasisrelowllem1  32379  ltflcei  32567  fzmul  32707  pclfinclN  34254  rabrenfdioph  36396  uun123p2  38058  isosctrlem1ALT  38192