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  3779  oacan  8485  omlimcl  8515  nnacan  8566  dif1en  9098  unfi  9107  en3lplem2  9534  le2tri3i  11275  ltaddsublt  11776  div12  11830  lemul12b  12010  zdivadd  12575  zdivmul  12576  elfz  13441  fzmmmeqm  13485  fzrev  13515  modmulnn  13821  digit2  14171  digit1  14172  faclbnd5  14233  hashfundm  14377  absdiflt  15253  absdifle  15254  dvds0lem  16205  dvdsmulc  16222  dvds2add  16229  dvds2sub  16230  dvdstr  16233  lcmdvds  16547  pospropd  18260  fmfil  23900  elfm  23903  psmettri2  24265  xmettri2  24296  stdbdmetval  24470  nmf2  24549  isclmi0  25066  iscvsi  25097  brbtwn  28984  colinearalglem3  28993  colinearalg  28995  isvciOLD  30667  nvtri  30757  nmooge0  30854  his7  31177  his2sub2  31180  braadd  32032  bramul  32033  cnlnadjlem2  32155  pjimai  32263  atcvati  32473  mdsymlem5  32494  bnj240  34875  bnj1189  35184  cusgredgex  35335  colineardim1  36274  ftc1anclem6  37946  brcnvrabga  38590  oaord3  43646  omord2com  43656  uun123p3  45163  stoweidlem2  46357  sigarperm  47215  leaddsuble  47654