Theorem 3com12 1185

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

Syntax hints:   -> wi 4   /\ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  3adant2l  1210  3adant2r  1211  brelrng  4765  funimaexglem  5201  fvun2  5481  nnaordi  6397  nnmword  6407  fpmg  6561  prcdnql  7285  prcunqu  7286  prarloc  7304  ltaprg  7420  mul12  7884  add12  7913  addsub  7966  addsubeq4  7970  ppncan  7997  leadd1  8185  ltaddsub2  8192  leaddsub2  8194  lemul1  8348  reapmul1lem  8349  reapadd1  8351  reapcotr  8353  remulext1  8354  div23ap  8444  ltmulgt11  8615  lediv1  8620  lemuldiv  8632  zdiv  9132  iooneg  9764  icoshft  9766  fzaddel  9832  fzshftral  9881  facwordi  10479  abssubge0  10867  climshftlemg  11064  dvdsmul1  11504  divalgb  11611  lcmgcdeq  11753  cnmptcom  12456  hmeof1o2  12466