Theorem 3comr 841

Description: Commutation in antecedent. Rotate right.

Hypothesis

Ref	Expression
3exp.1	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
3comr	|- ((ch /\ ph /\ ps) -> th)

Proof of Theorem 3comr

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3coml 840	. 2 |- ((ps /\ ch /\ ph) -> th)
3	2	3coml 840	1 |- ((ch /\ ph /\ ps) -> th)

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  oacan 4182  omlimcl 4209  le2tri3 5589  div12t 5744  lemul12ait 5842  seq1cl 6325  elfzt 6471  fzrevt 6511  absdifltt 6883  absdiflet 6884  faclbnd5 6953  climsqueeze 7140  tgss2t 7637  mettri2 7813  bcthlem8 8006  isvci 8201  nvtri 8298  va1cnlem 8345  nmoge0 8430  ubthlem12 8540  his7t 8956  his2sub2t 8959  hcau2 9055  pjspansnt 9500  braaddt 9869  bramult 9870  cnlnadjlem2 10001  pjima 10104  atcvat 10313  mdsymlem5 10334

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain