Theorem 3comr 843

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 842	. 2 |- ((ps /\ ch /\ ph) -> th)
3	2	3coml 842	1 |- ((ch /\ ph /\ ps) -> th)

Syntax hints:   -> wi 3   /\ w3a 777

This theorem is referenced by:  oacan 4188  omlimcl 4215  le2tri3 5601  div12t 5751  lemul12ait 5844  seq1cl 6326  elfzt 6472  fzrevt 6512  absdifltt 6883  absdiflet 6884  faclbnd5 6953  climsqueeze 7140  tgss2t 7636  mettri2 7810  bcthlem8 8003  isvci 8197  nvtri 8294  va1cnlem 8341  nmoge0 8426  ubthlem12 8536  his7t 8951  his2sub2t 8954  hcau2 9050  pjspansnt 9495  braaddt 9864  bramult 9865  cnlnadjlem2 9996  pjima 10099  atcvat 10308  mdsymlem5 10329

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 779

Copyright terms: Public domain