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  4893  iotam  5246  funimaexglem  5337  fvun2  5624  nnaordi  6561  nnmword  6571  fpmg  6728  prcdnql  7544  prcunqu  7545  prarloc  7563  ltaprg  7679  mul12  8148  add12  8177  addsub  8230  addsubeq4  8234  ppncan  8261  leadd1  8449  ltaddsub2  8456  leaddsub2  8458  lemul1  8612  reapmul1lem  8613  reapadd1  8615  reapcotr  8617  remulext1  8618  div23ap  8710  ltmulgt11  8883  lediv1  8888  lemuldiv  8900  zdiv  9405  iooneg  10054  icoshft  10056  fzaddel  10125  fzshftral  10174  facwordi  10811  abssubge0  11246  climshftlemg  11445  dvdsmul1  11956  divalgb  12066  lcmgcdeq  12221  pcfac  12488  mhmmulg  13233  rmodislmodlem  13846  cnmptcom  14466  hmeof1o2  14476