Theorem 3comr 1125

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  3com23  1126  sbciegft  3781  oacan  8473  omlimcl  8503  nnacan  8553  dif1en  9084  dif1enOLD  9086  unfi  9095  en3lplem2  9528  le2tri3i  11264  ltaddsublt  11765  div12  11819  lemul12b  11999  zdivadd  12565  zdivmul  12566  elfz  13434  fzmmmeqm  13478  fzrev  13508  modmulnn  13811  digit2  14161  digit1  14162  faclbnd5  14223  hashfundm  14367  absdiflt  15243  absdifle  15244  dvds0lem  16195  dvdsmulc  16212  dvds2add  16219  dvds2sub  16220  dvdstr  16223  lcmdvds  16537  pospropd  18249  fmfil  23847  elfm  23850  psmettri2  24213  xmettri2  24244  stdbdmetval  24418  nmf2  24497  isclmi0  25014  iscvsi  25045  brbtwn  28862  colinearalglem3  28871  colinearalg  28873  isvciOLD  30542  nvtri  30632  nmooge0  30729  his7  31052  his2sub2  31055  braadd  31907  bramul  31908  cnlnadjlem2  32030  pjimai  32138  atcvati  32348  mdsymlem5  32369  bnj240  34668  bnj1189  34978  cusgredgex  35097  colineardim1  36037  ftc1anclem6  37680  brcnvrabga  38312  oaord3  43268  omord2com  43278  uun123p3  44787  stoweidlem2  45987  sigarperm  46845  leaddsuble  47285