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  3603  omwordri  8610  oeword  8628  f1oen2g  9009  f1dom2g  9010  f1imaenfi  9235  ordiso  9556  en3lplem2  9653  axdc3lem4  10493  ltasr  11140  adddir  11252  axltadd  11334  pnpcan2  11549  subdir  11697  ltaddsub  11737  leaddsub  11739  mulcan2g  11917  div13  11943  ltdiv2  12154  lediv2  12158  zdiv  12688  xadddir  13338  xadddi2r  13340  fzen  13581  fzrevral2  13653  fzshftral  13655  ssfzoulel  13799  fzind2  13824  flflp1  13847  mulbinom2  14262  digit1  14276  faclbnd5  14337  ccatlcan  14756  elicc4abs  15358  dvdsnegb  16311  muldvds1  16318  muldvds2  16319  dvdscmul  16320  dvdsmulc  16321  dvdscmulr  16322  dvdsmulcr  16323  dvdsgcd  16581  mulgcdr  16587  lcmgcdeq  16649  congr  16701  mulgnnass  19127  gaass  19315  elfm3  23958  mettri  24362  cnmet  24792  addcnlem  24886  bcthlem5  25362  isppw2  27158  vmappw  27159  bcmono  27321  sletr  27803  sltadd1im  28018  colinearalg  28925  ax5seglem1  28943  ax5seglem2  28944  vcdir  30585  vcass  30586  imsmetlem  30709  hvaddcan2  31090  hvsubcan2  31094  dfgcd3  37325  isbasisrelowllem1  37356  ltflcei  37615  fzmul  37748  brcnvrabga  38343  pclfinclN  39952  rabrenfdioph  42825  uun123p2  44830  isosctrlem1ALT  44954