Theorem 3com12 1209

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

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 982

This theorem is referenced by:  3adant2l  1234  3adant2r  1235  brelrng  4898  iotam  5251  funimaexglem  5342  fvun2  5631  nnaordi  6575  nnmword  6585  fpmg  6742  prcdnql  7568  prcunqu  7569  prarloc  7587  ltaprg  7703  mul12  8172  add12  8201  addsub  8254  addsubeq4  8258  ppncan  8285  leadd1  8474  ltaddsub2  8481  leaddsub2  8483  lemul1  8637  reapmul1lem  8638  reapadd1  8640  reapcotr  8642  remulext1  8643  div23ap  8735  ltmulgt11  8908  lediv1  8913  lemuldiv  8925  zdiv  9431  iooneg  10080  icoshft  10082  fzaddel  10151  fzshftral  10200  facwordi  10849  abssubge0  11284  climshftlemg  11484  dvdsmul1  11995  divalgb  12107  lcmgcdeq  12276  pcfac  12544  mhmmulg  13369  rmodislmodlem  13982  cnmptcom  14618  hmeof1o2  14628