Theorem 3coml 1145

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  spc3egv  3561  omwordri  8611  oeword  8630  f1oen2g  9026  f1dom2g  9027  f1imaenfi  9241  ordiso  9540  en3lplem2  9644  axdc3lem4  10561  ltasr  11215  adddir  11327  axltadd  11413  pnpcan2  11628  subdir  11780  ltaddsub  11820  leaddsub  11822  mulcan2g  12000  div13  12025  ltdiv2  12233  lediv2  12237  zdiv  12799  xadddir  13456  xadddi2r  13458  fzen  13704  fzrevral2  13777  fzshftral  13779  ssfzoulel  13925  fzind2  13953  flflp1  13977  mulbinom2  14397  digit1  14411  faclbnd5  14472  ccatlcan  14898  elicc4abs  15519  dvdsnegb  16475  muldvds1  16482  muldvds2  16483  dvdscmul  16484  dvdsmulc  16485  dvdscmulr  16486  dvdsmulcr  16487  dvdsgcd  16749  mulgcdr  16755  lcmgcdeq  16819  congr  16871  mulgnnass  19351  gaass  19544  elfm3  24302  mettri  24704  cnmet  25123  addcnlem  25217  bcthlem5  25682  isppw2  27475  vmappw  27476  bcmono  27637  lestr  28152  ltadds1im  28404  colinearalg  29521  ax5seglem1  29539  ax5seglem2  29540  vcdir  31201  vcass  31202  imsmetlem  31325  hvaddcan2  31706  hvsubcan2  31710  nmulle  37157  naddle  37159  dfgcd3  38450  isbasisrelowllem1  38483  ltflcei  38736  fzmul  38878  brcnvrabga  39477  pclfinclN  41210  rabrenfdioph  44025  uun123p2  45994  isosctrlem1ALT  46118