Theorem 3comr 1131

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3com23  1132  sbciegft  3760  oacan  8473  omlimcl  8503  nnacan  8554  dif1en  9086  unfi  9095  en3lplem2  9525  le2tri3i  11267  ltaddsublt  11768  div12  11822  lemul12b  12003  zdivadd  12591  zdivmul  12592  elfz  13458  fzmmmeqm  13502  fzrev  13532  modmulnn  13839  digit2  14189  digit1  14190  faclbnd5  14251  hashfundm  14395  absdiflt  15271  absdifle  15272  dvds0lem  16226  dvdsmulc  16243  dvds2add  16250  dvds2sub  16251  dvdstr  16254  lcmdvds  16568  pospropd  18282  fmfil  23927  elfm  23930  psmettri2  24292  xmettri2  24323  stdbdmetval  24497  nmf2  24576  isclmi0  25083  iscvsi  25114  brbtwn  28986  colinearalglem3  28995  colinearalg  28997  isvciOLD  30669  nvtri  30759  nmooge0  30856  his7  31179  his2sub2  31182  braadd  32034  bramul  32035  cnlnadjlem2  32157  pjimai  32265  atcvati  32475  mdsymlem5  32496  bnj240  34882  bnj1189  35191  cusgredgex  35350  colineardim1  36289  ftc1anclem6  38065  brcnvrabga  38709  oaord3  43737  omord2com  43747  uun123p3  45254  stoweidlem2  46445  sigarperm  47303  leaddsuble  47760