Theorem 3comr 1124

Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.) (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 1122	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
3	2	3com13 1123	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  1125  sbciegft  3828  oacan  8584  omlimcl  8614  nnacan  8664  dif1en  9198  dif1enOLD  9200  unfi  9209  en3lplem2  9650  le2tri3i  11388  ltaddsublt  11887  div12  11941  lemul12b  12121  zdivadd  12686  zdivmul  12687  elfz  13549  fzmmmeqm  13593  fzrev  13623  modmulnn  13925  digit2  14271  digit1  14272  faclbnd5  14333  hashfundm  14477  absdiflt  15352  absdifle  15353  dvds0lem  16300  dvdsmulc  16317  dvds2add  16323  dvds2sub  16324  dvdstr  16327  lcmdvds  16641  pospropd  18384  fmfil  23967  elfm  23970  psmettri2  24334  xmettri2  24365  stdbdmetval  24542  nmf2  24621  isclmi0  25144  iscvsi  25175  brbtwn  28928  colinearalglem3  28937  colinearalg  28939  isvciOLD  30608  nvtri  30698  nmooge0  30795  his7  31118  his2sub2  31121  braadd  31973  bramul  31974  cnlnadjlem2  32096  pjimai  32204  atcvati  32414  mdsymlem5  32435  bnj240  34691  bnj1189  35001  cusgredgex  35105  colineardim1  36042  ftc1anclem6  37684  brcnvrabga  38323  oaord3  43281  omord2com  43291  uun123p3  44808  stoweidlem2  45957  sigarperm  46815  leaddsuble  47246