Theorem 3com12 1208

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 986	. 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 979

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 981

This theorem is referenced by:  3adant2l  1233  3adant2r  1234  brelrng  4870  iotam  5220  funimaexglem  5311  fvun2  5596  nnaordi  6522  nnmword  6532  fpmg  6687  prcdnql  7496  prcunqu  7497  prarloc  7515  ltaprg  7631  mul12  8099  add12  8128  addsub  8181  addsubeq4  8185  ppncan  8212  leadd1  8400  ltaddsub2  8407  leaddsub2  8409  lemul1  8563  reapmul1lem  8564  reapadd1  8566  reapcotr  8568  remulext1  8569  div23ap  8661  ltmulgt11  8834  lediv1  8839  lemuldiv  8851  zdiv  9354  iooneg  10001  icoshft  10003  fzaddel  10072  fzshftral  10121  facwordi  10733  abssubge0  11124  climshftlemg  11323  dvdsmul1  11833  divalgb  11943  lcmgcdeq  12096  pcfac  12361  mhmmulg  13055  rmodislmodlem  13534  cnmptcom  14069  hmeof1o2  14079