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  4909  iotam  5263  funimaexglem  5357  fvun2  5646  nnaordi  6594  nnmword  6604  fpmg  6761  prcdnql  7597  prcunqu  7598  prarloc  7616  ltaprg  7732  mul12  8201  add12  8230  addsub  8283  addsubeq4  8287  ppncan  8314  leadd1  8503  ltaddsub2  8510  leaddsub2  8512  lemul1  8666  reapmul1lem  8667  reapadd1  8669  reapcotr  8671  remulext1  8672  div23ap  8764  ltmulgt11  8937  lediv1  8942  lemuldiv  8954  zdiv  9461  iooneg  10110  icoshft  10112  fzaddel  10181  fzshftral  10230  facwordi  10885  abssubge0  11413  climshftlemg  11613  dvdsmul1  12124  divalgb  12236  lcmgcdeq  12405  pcfac  12673  mhmmulg  13499  rmodislmodlem  14112  cnmptcom  14770  hmeof1o2  14780