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  3790  oacan  8512  omlimcl  8542  nnacan  8592  dif1en  9124  dif1enOLD  9126  unfi  9135  en3lplem2  9566  le2tri3i  11304  ltaddsublt  11805  div12  11859  lemul12b  12039  zdivadd  12605  zdivmul  12606  elfz  13474  fzmmmeqm  13518  fzrev  13548  modmulnn  13851  digit2  14201  digit1  14202  faclbnd5  14263  hashfundm  14407  absdiflt  15284  absdifle  15285  dvds0lem  16236  dvdsmulc  16253  dvds2add  16260  dvds2sub  16261  dvdstr  16264  lcmdvds  16578  pospropd  18286  fmfil  23831  elfm  23834  psmettri2  24197  xmettri2  24228  stdbdmetval  24402  nmf2  24481  isclmi0  24998  iscvsi  25029  brbtwn  28826  colinearalglem3  28835  colinearalg  28837  isvciOLD  30509  nvtri  30599  nmooge0  30696  his7  31019  his2sub2  31022  braadd  31874  bramul  31875  cnlnadjlem2  31997  pjimai  32105  atcvati  32315  mdsymlem5  32336  bnj240  34689  bnj1189  34999  cusgredgex  35109  colineardim1  36049  ftc1anclem6  37692  brcnvrabga  38324  oaord3  43281  omord2com  43291  uun123p3  44800  stoweidlem2  46000  sigarperm  46858  leaddsuble  47298