Theorem 3com12 1197

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 975	. 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 968

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 970

This theorem is referenced by:  3adant2l  1222  3adant2r  1223  brelrng  4835  funimaexglem  5271  fvun2  5553  nnaordi  6476  nnmword  6486  fpmg  6640  prcdnql  7425  prcunqu  7426  prarloc  7444  ltaprg  7560  mul12  8027  add12  8056  addsub  8109  addsubeq4  8113  ppncan  8140  leadd1  8328  ltaddsub2  8335  leaddsub2  8337  lemul1  8491  reapmul1lem  8492  reapadd1  8494  reapcotr  8496  remulext1  8497  div23ap  8587  ltmulgt11  8759  lediv1  8764  lemuldiv  8776  zdiv  9279  iooneg  9924  icoshft  9926  fzaddel  9994  fzshftral  10043  facwordi  10653  abssubge0  11044  climshftlemg  11243  dvdsmul1  11753  divalgb  11862  lcmgcdeq  12015  pcfac  12280  cnmptcom  12938  hmeof1o2  12948