Theorem 3com12 837

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 832	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	com12 11	. 2 |- (ps -> (ph -> (ch -> th)))
4	3	3imp 827	1 |- ((ps /\ ph /\ ch) -> th)

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  3adant2l 854  3adant2r 855  relelrng 3347  ecopoprtrn 4311  add12t 5336  addsubt 5384  mul12t 5418  ppncant 5481  ltaddsub2t 5632  leaddsub2t 5634  lesub2t 5661  ltsub2t 5663  div23t 5742  divcan4tOLD 5763  divdivdivt 5785  ltmulgt11t 5846  lediv1t 5851  lediv1tOLD 5852  ltmuldiv2tOLD 5866  ltdivmultOLD 5868  ledivmultOLD 5869  lt2mul2divt 5872  lemuldivt 5874  lemuldivtOLD 5875  lemuldiv2tOLD 5877  ltdiv2t 5887  nndivt 5959  ioonegt 6406  icoshft 6408  fznn0subt 6498  fzaddelt 6500  fzshftralt 6522  abssubge0t 6895  facwordit 6944  bccl2t 6971  fsummulc2 7034  climcmplem 7137  climsqueeze 7140  climsqueeze2 7141  cvgcmp3c 7186  efaddlem24 7361  znnenlem 7501  2basgent 7641  ioo2bl 7912  tgioolem 7914  xplm 7975  isgrp2i 8076  vcdi 8171  isvci 8201  ipdi 8503  ipsubdi 8509  spwpr3OLD 8662  hvadd12t 8904  hvmulcomt 8912  his5t 8953  bcs3t 9050  chj12t 9457  homul12t 9731  hoaddsubt 9742  kbmult 9879  lnopmult 9891  lnopaddmul 9897  lnopsubmul 9899  homco2t 9901  lnfnaddmul 9974  leop2t 10057  dmdsl3t 10242  irredlem3 10319  atmd2 10327  cdj3lem3 10365  nndivsub 10421  cnvhmph 10527  hmphsyma 10528

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