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  3775  oacan  8560  omlimcl  8590  nnacan  8641  dif1en  9181  unfi  9190  en3lplem2  9618  le2tri3i  11444  ltaddsublt  11947  div12  12000  lemul12b  12178  zdivadd  12774  zdivmul  12775  elfz  13649  fzmmmeqm  13695  fzrev  13725  modmulnn  14033  digit2  14384  digit1  14385  faclbnd5  14446  hashfundm  14591  absdiflt  15491  absdifle  15492  dvds0lem  16442  dvdsmulc  16459  dvds2add  16466  dvds2sub  16467  dvdstr  16470  lcmdvds  16789  pospropd  18505  fmfil  24269  elfm  24272  psmettri2  24634  xmettri2  24665  stdbdmetval  24839  nmf2  24918  isclmi0  25425  iscvsi  25456  brbtwn  29483  colinearalglem3  29492  colinearalg  29494  isvciOLD  31188  nvtri  31278  nmooge0  31375  his7  31698  his2sub2  31701  braadd  32553  bramul  32554  cnlnadjlem2  32676  pjimai  32784  atcvati  32994  mdsymlem5  33015  bnj240  35377  bnj1189  35686  cusgredgex  35983  colineardim1  36919  ftc1anclem6  38710  brcnvrabga  39368  oaord3  44388  omord2com  44398  uun123p3  45887  stoweidlem2  47106  sigarperm  47964  leaddsuble  48461