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  3793  oacan  8515  omlimcl  8545  nnacan  8595  dif1en  9130  dif1enOLD  9132  unfi  9141  en3lplem2  9573  le2tri3i  11311  ltaddsublt  11812  div12  11866  lemul12b  12046  zdivadd  12612  zdivmul  12613  elfz  13481  fzmmmeqm  13525  fzrev  13555  modmulnn  13858  digit2  14208  digit1  14209  faclbnd5  14270  hashfundm  14414  absdiflt  15291  absdifle  15292  dvds0lem  16243  dvdsmulc  16260  dvds2add  16267  dvds2sub  16268  dvdstr  16271  lcmdvds  16585  pospropd  18293  fmfil  23838  elfm  23841  psmettri2  24204  xmettri2  24235  stdbdmetval  24409  nmf2  24488  isclmi0  25005  iscvsi  25036  brbtwn  28833  colinearalglem3  28842  colinearalg  28844  isvciOLD  30516  nvtri  30606  nmooge0  30703  his7  31026  his2sub2  31029  braadd  31881  bramul  31882  cnlnadjlem2  32004  pjimai  32112  atcvati  32322  mdsymlem5  32343  bnj240  34696  bnj1189  35006  cusgredgex  35116  colineardim1  36056  ftc1anclem6  37699  brcnvrabga  38331  oaord3  43288  omord2com  43298  uun123p3  44807  stoweidlem2  46007  sigarperm  46865  leaddsuble  47302