Theorem 3com12 1202

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 980	. 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 973

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

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

This theorem is referenced by:  3adant2l  1227  3adant2r  1228  brelrng  4842  iotam  5190  funimaexglem  5281  fvun2  5563  nnaordi  6487  nnmword  6497  fpmg  6652  prcdnql  7446  prcunqu  7447  prarloc  7465  ltaprg  7581  mul12  8048  add12  8077  addsub  8130  addsubeq4  8134  ppncan  8161  leadd1  8349  ltaddsub2  8356  leaddsub2  8358  lemul1  8512  reapmul1lem  8513  reapadd1  8515  reapcotr  8517  remulext1  8518  div23ap  8608  ltmulgt11  8780  lediv1  8785  lemuldiv  8797  zdiv  9300  iooneg  9945  icoshft  9947  fzaddel  10015  fzshftral  10064  facwordi  10674  abssubge0  11066  climshftlemg  11265  dvdsmul1  11775  divalgb  11884  lcmgcdeq  12037  pcfac  12302  cnmptcom  13092  hmeof1o2  13102