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  3559  omwordri  8509  oeword  8528  f1oen2g  8917  f1dom2g  8918  f1imaenfi  9131  ordiso  9433  en3lplem2  9534  axdc3lem4  10375  ltasr  11023  adddir  11135  axltadd  11218  pnpcan2  11433  subdir  11583  ltaddsub  11623  leaddsub  11625  mulcan2g  11803  div13  11829  ltdiv2  12040  lediv2  12044  zdiv  12574  xadddir  13223  xadddi2r  13225  fzen  13469  fzrevral2  13541  fzshftral  13543  ssfzoulel  13688  fzind2  13716  flflp1  13739  mulbinom2  14158  digit1  14172  faclbnd5  14233  ccatlcan  14653  elicc4abs  15255  dvdsnegb  16212  muldvds1  16219  muldvds2  16220  dvdscmul  16221  dvdsmulc  16222  dvdscmulr  16223  dvdsmulcr  16224  dvdsgcd  16483  mulgcdr  16489  lcmgcdeq  16551  congr  16603  mulgnnass  19051  gaass  19238  elfm3  23906  mettri  24308  cnmet  24727  addcnlem  24821  bcthlem5  25296  isppw2  27093  vmappw  27094  bcmono  27256  lestr  27742  ltadds1im  27993  colinearalg  28995  ax5seglem1  29013  ax5seglem2  29014  vcdir  30653  vcass  30654  imsmetlem  30777  hvaddcan2  31158  hvsubcan2  31162  dfgcd3  37573  isbasisrelowllem1  37604  ltflcei  37853  fzmul  37986  brcnvrabga  38587  pclfinclN  40320  rabrenfdioph  43165  uun123p2  45159  isosctrlem1ALT  45283