Theorem 3com12 1168

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

Syntax hints:   -> wi 4   /\ w3a 945

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

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  3adant2l  1193  3adant2r  1194  brelrng  4730  funimaexglem  5164  fvun2  5442  nnaordi  6358  nnmword  6368  fpmg  6522  prcdnql  7240  prcunqu  7241  prarloc  7259  ltaprg  7375  mul12  7814  add12  7843  addsub  7896  addsubeq4  7900  ppncan  7927  leadd1  8111  ltaddsub2  8118  leaddsub2  8120  lemul1  8273  reapmul1lem  8274  reapadd1  8276  reapcotr  8278  remulext1  8279  div23ap  8364  ltmulgt11  8532  lediv1  8537  lemuldiv  8549  zdiv  9043  iooneg  9664  icoshft  9666  fzaddel  9732  fzshftral  9781  facwordi  10379  abssubge0  10766  climshftlemg  10963  dvdsmul1  11363  divalgb  11470  lcmgcdeq  11610  cnmptcom  12309