Theorem 3com12 1142

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 926	. 2 |- ( ( ps /\ ph /\ ch ) <-> ( ph /\ ps /\ ch ) )
2		3exp.1	. 2 |- ( ( ph /\ ps /\ ch ) -> th )
3	1, 2	sylbi 119	1 |- ( ( ps /\ ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  3adant2l  1163  3adant2r  1164  brelrng  4583  funimaexglem  5002  fvun2  5261  nnaordi  6104  nnmword  6114  prcdnql  6674  prcunqu  6675  prarloc  6693  ltaprg  6809  mul12  7237  add12  7266  addsub  7319  addsubeq4  7323  ppncan  7350  leadd1  7534  ltaddsub2  7541  leaddsub2  7543  lemul1  7693  reapmul1lem  7694  reapadd1  7696  reapcotr  7698  remulext1  7699  div23ap  7779  ltmulgt11  7942  lediv1  7947  lemuldiv  7959  zdiv  8435  iooneg  9010  icoshft  9012  fzaddel  9077  fzshftral  9125  facwordi  9667  abssubge0  9988  climshftlemg  10141  dvdsmul1  10217  divalgb  10325  lcmgcdeq  10465