Theorem 3comr 1126

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3com23  1127  sbciegft  3766  oacan  8476  omlimcl  8506  nnacan  8557  dif1en  9089  unfi  9098  en3lplem2  9525  le2tri3i  11267  ltaddsublt  11768  div12  11822  lemul12b  12003  zdivadd  12591  zdivmul  12592  elfz  13458  fzmmmeqm  13502  fzrev  13532  modmulnn  13839  digit2  14189  digit1  14190  faclbnd5  14251  hashfundm  14395  absdiflt  15271  absdifle  15272  dvds0lem  16226  dvdsmulc  16243  dvds2add  16250  dvds2sub  16251  dvdstr  16254  lcmdvds  16568  pospropd  18282  fmfil  23919  elfm  23922  psmettri2  24284  xmettri2  24315  stdbdmetval  24489  nmf2  24568  isclmi0  25075  iscvsi  25106  brbtwn  28982  colinearalglem3  28991  colinearalg  28993  isvciOLD  30666  nvtri  30756  nmooge0  30853  his7  31176  his2sub2  31179  braadd  32031  bramul  32032  cnlnadjlem2  32154  pjimai  32262  atcvati  32472  mdsymlem5  32493  bnj240  34858  bnj1189  35167  cusgredgex  35320  colineardim1  36259  ftc1anclem6  38033  brcnvrabga  38677  oaord3  43738  omord2com  43748  uun123p3  45255  stoweidlem2  46448  sigarperm  47306  leaddsuble  47757