Theorem 3comr 1143

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3com23  1144  sbciegft  3776  oacan  8535  omlimcl  8565  nnacan  8616  dif1en  9156  unfi  9165  en3lplem2  9592  le2tri3i  11364  ltaddsublt  11865  div12  11918  lemul12b  12096  zdivadd  12692  zdivmul  12693  elfz  13567  fzmmmeqm  13612  fzrev  13642  modmulnn  13950  digit2  14300  digit1  14301  faclbnd5  14362  hashfundm  14507  absdiflt  15405  absdifle  15406  dvds0lem  16356  dvdsmulc  16373  dvds2add  16380  dvds2sub  16381  dvdstr  16384  lcmdvds  16698  pospropd  18413  fmfil  24170  elfm  24173  psmettri2  24535  xmettri2  24566  stdbdmetval  24740  nmf2  24819  isclmi0  25326  iscvsi  25357  brbtwn  29356  colinearalglem3  29365  colinearalg  29367  isvciOLD  31061  nvtri  31151  nmooge0  31248  his7  31571  his2sub2  31574  braadd  32426  bramul  32427  cnlnadjlem2  32549  pjimai  32657  atcvati  32867  mdsymlem5  32888  bnj240  35209  bnj1189  35518  cusgredgex  35720  colineardim1  36641  ftc1anclem6  38447  brcnvrabga  39090  oaord3  44133  omord2com  44143  uun123p3  45633  stoweidlem2  46830  sigarperm  47688  leaddsuble  48185