Theorem 3com12 1209

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

Syntax hints:   -> wi 4   /\ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  3adant2l  1234  3adant2r  1235  brelrng  4897  iotam  5250  funimaexglem  5341  fvun2  5628  nnaordi  6566  nnmword  6576  fpmg  6733  prcdnql  7551  prcunqu  7552  prarloc  7570  ltaprg  7686  mul12  8155  add12  8184  addsub  8237  addsubeq4  8241  ppncan  8268  leadd1  8457  ltaddsub2  8464  leaddsub2  8466  lemul1  8620  reapmul1lem  8621  reapadd1  8623  reapcotr  8625  remulext1  8626  div23ap  8718  ltmulgt11  8891  lediv1  8896  lemuldiv  8908  zdiv  9414  iooneg  10063  icoshft  10065  fzaddel  10134  fzshftral  10183  facwordi  10832  abssubge0  11267  climshftlemg  11467  dvdsmul1  11978  divalgb  12090  lcmgcdeq  12251  pcfac  12519  mhmmulg  13293  rmodislmodlem  13906  cnmptcom  14534  hmeof1o2  14544