Theorem 3com12 1234

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 1012	. 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 1005

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 1007

This theorem is referenced by:  3adant2l  1259  3adant2r  1260  brelrng  4969  iotam  5325  funimaexglem  5420  fvun2  5722  nnaordi  6719  nnmword  6729  fpmg  6886  prcdnql  7747  prcunqu  7748  prarloc  7766  ltaprg  7882  mul12  8351  add12  8380  addsub  8433  addsubeq4  8437  ppncan  8464  leadd1  8653  ltaddsub2  8660  leaddsub2  8662  lemul1  8816  reapmul1lem  8817  reapadd1  8819  reapcotr  8821  remulext1  8822  div23ap  8914  ltmulgt11  9087  lediv1  9092  lemuldiv  9104  zdiv  9613  iooneg  10268  icoshft  10270  fzaddel  10339  fzshftral  10388  facwordi  11048  pfxeq  11326  abssubge0  11725  climshftlemg  11925  dvdsmul1  12437  divalgb  12549  lcmgcdeq  12718  pcfac  12986  mhmmulg  13813  rmodislmodlem  14429  cnmptcom  15092  hmeof1o2  15102