Theorem 3com12 1207

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 985	. 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 978

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 980

This theorem is referenced by:  3adant2l  1232  3adant2r  1233  brelrng  4858  iotam  5208  funimaexglem  5299  fvun2  5583  nnaordi  6508  nnmword  6518  fpmg  6673  prcdnql  7482  prcunqu  7483  prarloc  7501  ltaprg  7617  mul12  8085  add12  8114  addsub  8167  addsubeq4  8171  ppncan  8198  leadd1  8386  ltaddsub2  8393  leaddsub2  8395  lemul1  8549  reapmul1lem  8550  reapadd1  8552  reapcotr  8554  remulext1  8555  div23ap  8647  ltmulgt11  8820  lediv1  8825  lemuldiv  8837  zdiv  9340  iooneg  9987  icoshft  9989  fzaddel  10058  fzshftral  10107  facwordi  10719  abssubge0  11110  climshftlemg  11309  dvdsmul1  11819  divalgb  11929  lcmgcdeq  12082  pcfac  12347  mhmmulg  13022  cnmptcom  13768  hmeof1o2  13778