Theorem 3com12 835

Description: Commutation in antecedent. Swap 1st and 3rd.

Hypothesis

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

Assertion

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

Proof of Theorem 3com12

Step	Hyp	Ref	Expression
1		3exp.1	. . . 4 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 830	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	com12 11	. 2 |- (ps -> (ph -> (ch -> th)))
4	3	3imp 825	1 |- ((ps /\ ph /\ ch) -> th)

Syntax hints:   -> wi 3   /\ w3a 773

This theorem is referenced by:  3adant2l 852  3adant2r 853  ecopoprtrn 4295  add12t 5308  addsubt 5356  mul12t 5390  ppncant 5453  ltaddsub2t 5606  leaddsub2t 5608  lesub2t 5634  ltsub2t 5636  div23t 5705  divmuldivt 5736  divdivdivt 5741  ltmulgt11t 5802  lediv1t 5806  ltmuldiv2t 5818  lt2mul2divt 5822  lemuldivt 5824  lemuldiv2t 5825  ltdiv2t 5835  ltdiv23t 5840  lediv23t 5841  icoshft 6341  fznn0subt 6430  fzaddelt 6432  fzshftralt 6454  abssubge0t 6833  facwordit 6881  bccl2t 6909  fsummulc2 6972  climcmplem 7073  climsqueeze 7076  climsqueeze2 7077  cvgcmp3c 7122  efaddlem24 7303  znnenlem 7443  2basgent 7583  ioo2bl 7851  tgioolem 7853  xplm 7909  isgrp2i 8011  vcdi 8108  isvci 8139  ipdi 8434  ipsubdi 8440  hvadd12t 8825  hvmulcomt 8833  his5t 8874  bcs3t 8971  chj12t 9372  homul12t 9648  hoaddsubt 9659  kbmult 9795  lnopmult 9807  lnopaddmul 9813  lnopsubmul 9815  homco2t 9817  lnfnaddmul 9889  leop2t 9969  dmdsl3t 10150  irredlem3 10227  atmd2 10235  cdj3lem3 10270  cnvhmph 10414  hmphsyma 10415

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 775

Copyright terms: Public domain