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  4928  iotam  5282  funimaexglem  5376  fvun2  5669  nnaordi  6617  nnmword  6627  fpmg  6784  prcdnql  7632  prcunqu  7633  prarloc  7651  ltaprg  7767  mul12  8236  add12  8265  addsub  8318  addsubeq4  8322  ppncan  8349  leadd1  8538  ltaddsub2  8545  leaddsub2  8547  lemul1  8701  reapmul1lem  8702  reapadd1  8704  reapcotr  8706  remulext1  8707  div23ap  8799  ltmulgt11  8972  lediv1  8977  lemuldiv  8989  zdiv  9496  iooneg  10145  icoshft  10147  fzaddel  10216  fzshftral  10265  facwordi  10922  pfxeq  11187  abssubge0  11528  climshftlemg  11728  dvdsmul1  12239  divalgb  12351  lcmgcdeq  12520  pcfac  12788  mhmmulg  13614  rmodislmodlem  14227  cnmptcom  14885  hmeof1o2  14895