Theorem 3com12 1189

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 970	. 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 963

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 965

This theorem is referenced by:  3adant2l  1214  3adant2r  1215  brelrng  4819  funimaexglem  5255  fvun2  5537  nnaordi  6457  nnmword  6467  fpmg  6621  prcdnql  7406  prcunqu  7407  prarloc  7425  ltaprg  7541  mul12  8008  add12  8037  addsub  8090  addsubeq4  8094  ppncan  8121  leadd1  8309  ltaddsub2  8316  leaddsub2  8318  lemul1  8472  reapmul1lem  8473  reapadd1  8475  reapcotr  8477  remulext1  8478  div23ap  8568  ltmulgt11  8740  lediv1  8745  lemuldiv  8757  zdiv  9257  iooneg  9898  icoshft  9900  fzaddel  9967  fzshftral  10016  facwordi  10625  abssubge0  11013  climshftlemg  11210  dvdsmul1  11720  divalgb  11828  lcmgcdeq  11975  cnmptcom  12768  hmeof1o2  12778