Theorem 3comr 1137

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  3com23  1138  sbciegft  3779  oacan  8511  omlimcl  8541  nnacan  8592  dif1en  9124  unfi  9133  en3lplem2  9562  le2tri3i  11307  ltaddsublt  11808  div12  11861  lemul12b  12042  zdivadd  12638  zdivmul  12639  elfz  13512  fzmmmeqm  13556  fzrev  13586  modmulnn  13893  digit2  14243  digit1  14244  faclbnd5  14305  hashfundm  14449  absdiflt  15336  absdifle  15337  dvds0lem  16291  dvdsmulc  16308  dvds2add  16315  dvds2sub  16316  dvdstr  16319  lcmdvds  16633  pospropd  18348  fmfil  23992  elfm  23995  psmettri2  24357  xmettri2  24388  stdbdmetval  24562  nmf2  24641  isclmi0  25148  iscvsi  25179  brbtwn  29057  colinearalglem3  29066  colinearalg  29068  isvciOLD  30740  nvtri  30830  nmooge0  30927  his7  31250  his2sub2  31253  braadd  32105  bramul  32106  cnlnadjlem2  32228  pjimai  32336  atcvati  32546  mdsymlem5  32567  bnj240  34956  bnj1189  35265  cusgredgex  35433  colineardim1  36372  ftc1anclem6  38158  brcnvrabga  38802  oaord3  43830  omord2com  43840  uun123p3  45347  stoweidlem2  46537  sigarperm  47395  leaddsuble  47852