Theorem 3coml 1123

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  spc3egv  3604  omwordri  8198  oeword  8216  f1oen2g  8526  f1dom2g  8527  ordiso  8980  en3lplem2  9076  axdc3lem4  9875  ltasr  10522  adddir  10632  axltadd  10714  pnpcan2  10926  subdir  11074  ltaddsub  11114  leaddsub  11116  mulcan2g  11294  div13  11319  ltdiv2  11526  lediv2  11530  zdiv  12053  xadddir  12690  xadddi2r  12692  fzen  12925  fzrevral2  12994  fzshftral  12996  ssfzoulel  13132  fzind2  13156  flflp1  13178  mulbinom2  13585  digit1  13599  faclbnd5  13659  ccatlcan  14080  relexpreld  14399  elicc4abs  14679  dvdsnegb  15627  muldvds1  15634  muldvds2  15635  dvdscmul  15636  dvdsmulc  15637  dvdscmulr  15638  dvdsmulcr  15639  dvdsgcd  15892  mulgcdr  15898  lcmgcdeq  15956  congr  16008  mulgnnass  18262  gaass  18427  elfm3  22558  mettri  22962  cnmet  23380  addcnlem  23472  bcthlem5  23931  isppw2  25692  vmappw  25693  bcmono  25853  colinearalg  26696  ax5seglem1  26714  ax5seglem2  26715  vcdir  28343  vcass  28344  imsmetlem  28467  hvaddcan2  28848  hvsubcan2  28852  sletr  33237  dfgcd3  34608  isbasisrelowllem1  34639  ltflcei  34895  fzmul  35031  brcnvrabga  35614  pclfinclN  37101  rabrenfdioph  39431  uun123p2  41164  isosctrlem1ALT  41288