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  7764  prcunqu  7765  prarloc  7783  ltaprg  7899  mul12  8367  add12  8396  addsub  8449  addsubeq4  8453  ppncan  8480  leadd1  8669  ltaddsub2  8676  leaddsub2  8678  lemul1  8832  reapmul1lem  8833  reapadd1  8835  reapcotr  8837  remulext1  8838  div23ap  8930  ltmulgt11  9103  lediv1  9108  lemuldiv  9120  zdiv  9629  iooneg  10284  icoshft  10286  fzaddel  10356  fzshftral  10405  facwordi  11065  pfxeq  11343  abssubge0  11742  climshftlemg  11942  dvdsmul1  12454  divalgb  12566  lcmgcdeq  12735  pcfac  13003  mhmmulg  13830  rmodislmodlem  14446  cnmptcom  15109  hmeof1o2  15119