Theorem 3com12 1143

Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)

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		3ancoma 927	. 2 |- ( ( ps /\ ph /\ ch ) <-> ( ph /\ ps /\ ch ) )
2		3exp.1	. 2 |- ( ( ph /\ ps /\ ch ) -> th )
3	1, 2	sylbi 119	1 |- ( ( ps /\ ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ w3a 920

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  3adant2l  1164  3adant2r  1165  brelrng  4613  funimaexglem  5033  fvun2  5292  nnaordi  6168  nnmword  6178  prcdnql  6788  prcunqu  6789  prarloc  6807  ltaprg  6923  mul12  7356  add12  7385  addsub  7438  addsubeq4  7442  ppncan  7469  leadd1  7653  ltaddsub2  7660  leaddsub2  7662  lemul1  7812  reapmul1lem  7813  reapadd1  7815  reapcotr  7817  remulext1  7818  div23ap  7898  ltmulgt11  8061  lediv1  8066  lemuldiv  8078  zdiv  8568  iooneg  9138  icoshft  9140  fzaddel  9205  fzshftral  9253  facwordi  9816  abssubge0  10189  climshftlemg  10342  dvdsmul1  10425  divalgb  10532  lcmgcdeq  10672