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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3com23  1125  oacan  8379  omlimcl  8409  nnacan  8459  dif1en  8945  unfi  8955  en3lplem2  9371  le2tri3i  11105  ltaddsublt  11602  div12  11655  lemul12b  11832  zdivadd  12391  zdivmul  12392  elfz  13245  fzmmmeqm  13289  fzrev  13319  modmulnn  13609  digit2  13951  digit1  13952  faclbnd5  14012  absdiflt  15029  absdifle  15030  dvds0lem  15976  dvdsmulc  15993  dvds2add  15999  dvds2sub  16000  dvdstr  16003  lcmdvds  16313  pospropd  18045  fmfil  23095  elfm  23098  psmettri2  23462  xmettri2  23493  stdbdmetval  23670  nmf2  23749  isclmi0  24261  iscvsi  24292  brbtwn  27267  colinearalglem3  27276  colinearalg  27278  isvciOLD  28942  nvtri  29032  nmooge0  29129  his7  29452  his2sub2  29455  braadd  30307  bramul  30308  cnlnadjlem2  30430  pjimai  30538  atcvati  30748  mdsymlem5  30769  bnj240  32678  bnj1189  32989  hashfundm  33074  cusgredgex  33083  colineardim1  34363  ftc1anclem6  35855  brcnvrabga  36477  uun123p3  42431  stoweidlem2  43543  sigarperm  44376  leaddsuble  44789