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  4894  iotam  5247  funimaexglem  5338  fvun2  5625  nnaordi  6563  nnmword  6573  fpmg  6730  prcdnql  7546  prcunqu  7547  prarloc  7565  ltaprg  7681  mul12  8150  add12  8179  addsub  8232  addsubeq4  8236  ppncan  8263  leadd1  8451  ltaddsub2  8458  leaddsub2  8460  lemul1  8614  reapmul1lem  8615  reapadd1  8617  reapcotr  8619  remulext1  8620  div23ap  8712  ltmulgt11  8885  lediv1  8890  lemuldiv  8902  zdiv  9408  iooneg  10057  icoshft  10059  fzaddel  10128  fzshftral  10177  facwordi  10814  abssubge0  11249  climshftlemg  11448  dvdsmul1  11959  divalgb  12069  lcmgcdeq  12224  pcfac  12491  mhmmulg  13236  rmodislmodlem  13849  cnmptcom  14477  hmeof1o2  14487