Theorem 3comr 1143

Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.) Theorems shortened and reordered. (Revised by Wolf Lammen, 9-Apr-2022.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3comr	⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem 3comr

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3com12 1141	. 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:  3com23  1144  sbciegft  3783  oacan  8535  omlimcl  8565  nnacan  8616  dif1en  9149  unfi  9158  en3lplem2  9585  le2tri3i  11351  ltaddsublt  11852  div12  11905  lemul12b  12083  zdivadd  12678  zdivmul  12679  elfz  13552  fzmmmeqm  13597  fzrev  13627  modmulnn  13935  digit2  14285  digit1  14286  faclbnd5  14347  hashfundm  14492  absdiflt  15388  absdifle  15389  dvds0lem  16341  dvdsmulc  16358  dvds2add  16365  dvds2sub  16366  dvdstr  16369  lcmdvds  16683  pospropd  18398  fmfil  24130  elfm  24133  psmettri2  24495  xmettri2  24526  stdbdmetval  24700  nmf2  24779  isclmi0  25286  iscvsi  25317  brbtwn  29278  colinearalglem3  29287  colinearalg  29289  isvciOLD  30961  nvtri  31051  nmooge0  31148  his7  31471  his2sub2  31474  braadd  32326  bramul  32327  cnlnadjlem2  32449  pjimai  32557  atcvati  32767  mdsymlem5  32788  bnj240  35112  bnj1189  35421  cusgredgex  35627  colineardim1  36566  ftc1anclem6  38382  brcnvrabga  39024  oaord3  44052  omord2com  44062  uun123p3  45552  stoweidlem2  46749  sigarperm  47607  leaddsuble  48067