Theorem 3coml 1075

Description: Commutation in antecedent. Rotate left.

Hypothesis

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

Assertion

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

Proof of Theorem 3coml

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3com23 1074	. 2 |- ((ph /\ ch /\ ps) -> th)
3	2	3com13 1073	1 |- ((ps /\ ch /\ ph) -> th)

Syntax hints:   -> wi 3   /\ w3a 858

This theorem is referenced by:  3comr 1076  funbrfvbg 4716  oawordOLD 5231  omwordri 5251  ltapq 6228  ltmpq 6229  ltasr 6361  adddir 6472  addcan2 6508  subdir 6591  nnncan1OLD 6633  pnpcan2 6646  axltadd 6674  ltaddsub 6814  leaddsub 6816  lesub2 6850  ltsub2 6852  div13 6926  ltdiv2 7070  lediv2 7074  nndiv 7143  lble 7256  zdiv 7397  qbtwnre 7459  iooin 7539  iooss2 7541  fzen 7664  fzrevral2 7699  fzshftral 7701  digit1 7905  faclbnd5 8205  isummulc1iALT 8474  rescncf 8534  mettri 9094  metxp 9111  cnmet 9182  bl2ioo 9189  ghgrpi 9445  vcdir 9504  vcass 9505  imsmetlem 9655  elfilmap3 10314  hvaddcan2 10570  hvsubcan2 10575  pjeq2 10874  bnj245 12084  bnj847 12721  dvdsnegb 13672  muldvds1 13678  muldvds2 13679  dvdscmul 13680  dvdsmulc 13681  dvdscmulr 13682  dvdsmulcr 13683  coprmdvds 13783  fzmul 15790

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 164  df-an 242  df-3an 860

Copyright terms: Public domain