Theorem 3com12 1210

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 988	. 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 981

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 983

This theorem is referenced by:  3adant2l  1235  3adant2r  1236  brelrng  4910  iotam  5264  funimaexglem  5358  fvun2  5648  nnaordi  6596  nnmword  6606  fpmg  6763  prcdnql  7599  prcunqu  7600  prarloc  7618  ltaprg  7734  mul12  8203  add12  8232  addsub  8285  addsubeq4  8289  ppncan  8316  leadd1  8505  ltaddsub2  8512  leaddsub2  8514  lemul1  8668  reapmul1lem  8669  reapadd1  8671  reapcotr  8673  remulext1  8674  div23ap  8766  ltmulgt11  8939  lediv1  8944  lemuldiv  8956  zdiv  9463  iooneg  10112  icoshft  10114  fzaddel  10183  fzshftral  10232  facwordi  10887  pfxeq  11150  abssubge0  11446  climshftlemg  11646  dvdsmul1  12157  divalgb  12269  lcmgcdeq  12438  pcfac  12706  mhmmulg  13532  rmodislmodlem  14145  cnmptcom  14803  hmeof1o2  14813