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  3825  oacan  8586  omlimcl  8616  nnacan  8666  dif1en  9200  dif1enOLD  9202  unfi  9211  en3lplem2  9653  le2tri3i  11391  ltaddsublt  11890  div12  11944  lemul12b  12124  zdivadd  12689  zdivmul  12690  elfz  13553  fzmmmeqm  13597  fzrev  13627  modmulnn  13929  digit2  14275  digit1  14276  faclbnd5  14337  hashfundm  14481  absdiflt  15356  absdifle  15357  dvds0lem  16304  dvdsmulc  16321  dvds2add  16327  dvds2sub  16328  dvdstr  16331  lcmdvds  16645  pospropd  18372  fmfil  23952  elfm  23955  psmettri2  24319  xmettri2  24350  stdbdmetval  24527  nmf2  24606  isclmi0  25131  iscvsi  25162  brbtwn  28914  colinearalglem3  28923  colinearalg  28925  isvciOLD  30599  nvtri  30689  nmooge0  30786  his7  31109  his2sub2  31112  braadd  31964  bramul  31965  cnlnadjlem2  32087  pjimai  32195  atcvati  32405  mdsymlem5  32426  bnj240  34713  bnj1189  35023  cusgredgex  35127  colineardim1  36062  ftc1anclem6  37705  brcnvrabga  38343  oaord3  43305  omord2com  43315  uun123p3  44831  stoweidlem2  46017  sigarperm  46875  leaddsuble  47309