Theorem 3comr 1126

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 1124	. 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:  3com23  1127  sbciegft  3765  oacan  8483  omlimcl  8513  nnacan  8564  dif1en  9096  unfi  9105  en3lplem2  9534  le2tri3i  11276  ltaddsublt  11777  div12  11831  lemul12b  12012  zdivadd  12600  zdivmul  12601  elfz  13467  fzmmmeqm  13511  fzrev  13541  modmulnn  13848  digit2  14198  digit1  14199  faclbnd5  14260  hashfundm  14404  absdiflt  15280  absdifle  15281  dvds0lem  16235  dvdsmulc  16252  dvds2add  16259  dvds2sub  16260  dvdstr  16263  lcmdvds  16577  pospropd  18291  fmfil  23909  elfm  23912  psmettri2  24274  xmettri2  24305  stdbdmetval  24479  nmf2  24558  isclmi0  25065  iscvsi  25096  brbtwn  28968  colinearalglem3  28977  colinearalg  28979  isvciOLD  30651  nvtri  30741  nmooge0  30838  his7  31161  his2sub2  31164  braadd  32016  bramul  32017  cnlnadjlem2  32139  pjimai  32247  atcvati  32457  mdsymlem5  32478  bnj240  34842  bnj1189  35151  cusgredgex  35304  colineardim1  36243  ftc1anclem6  38019  brcnvrabga  38663  oaord3  43720  omord2com  43730  uun123p3  45237  stoweidlem2  46430  sigarperm  47288  leaddsuble  47745