Theorem 3com12 1231

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 1009	. 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 1002

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 1004

This theorem is referenced by:  3adant2l  1256  3adant2r  1257  brelrng  4955  iotam  5310  funimaexglem  5404  fvun2  5703  nnaordi  6662  nnmword  6672  fpmg  6829  prcdnql  7682  prcunqu  7683  prarloc  7701  ltaprg  7817  mul12  8286  add12  8315  addsub  8368  addsubeq4  8372  ppncan  8399  leadd1  8588  ltaddsub2  8595  leaddsub2  8597  lemul1  8751  reapmul1lem  8752  reapadd1  8754  reapcotr  8756  remulext1  8757  div23ap  8849  ltmulgt11  9022  lediv1  9027  lemuldiv  9039  zdiv  9546  iooneg  10196  icoshft  10198  fzaddel  10267  fzshftral  10316  facwordi  10974  pfxeq  11244  abssubge0  11629  climshftlemg  11829  dvdsmul1  12340  divalgb  12452  lcmgcdeq  12621  pcfac  12889  mhmmulg  13716  rmodislmodlem  14330  cnmptcom  14988  hmeof1o2  14998