Theorem 3comr 1141

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3com23  1142  sbciegft  3790  oacan  8529  omlimcl  8559  nnacan  8610  dif1en  9142  unfi  9151  en3lplem2  9578  le2tri3i  11336  ltaddsublt  11837  div12  11890  lemul12b  12068  zdivadd  12663  zdivmul  12664  elfz  13537  fzmmmeqm  13581  fzrev  13611  modmulnn  13918  digit2  14268  digit1  14269  faclbnd5  14330  hashfundm  14475  absdiflt  15365  absdifle  15366  dvds0lem  16320  dvdsmulc  16337  dvds2add  16344  dvds2sub  16345  dvdstr  16348  lcmdvds  16662  pospropd  18377  fmfil  24066  elfm  24069  psmettri2  24431  xmettri2  24462  stdbdmetval  24636  nmf2  24715  isclmi0  25222  iscvsi  25253  brbtwn  29186  colinearalglem3  29195  colinearalg  29197  isvciOLD  30869  nvtri  30959  nmooge0  31056  his7  31379  his2sub2  31382  braadd  32234  bramul  32235  cnlnadjlem2  32357  pjimai  32465  atcvati  32675  mdsymlem5  32696  bnj240  35029  bnj1189  35338  cusgredgex  35509  colineardim1  36448  ftc1anclem6  38232  brcnvrabga  38876  oaord3  43904  omord2com  43914  uun123p3  45404  stoweidlem2  46601  sigarperm  47459  leaddsuble  47916