Theorem 3com12 1233

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 1011	. 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 1004

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 1006

This theorem is referenced by:  3adant2l  1258  3adant2r  1259  brelrng  4963  iotam  5318  funimaexglem  5413  fvun2  5713  nnaordi  6676  nnmword  6686  fpmg  6843  prcdnql  7704  prcunqu  7705  prarloc  7723  ltaprg  7839  mul12  8308  add12  8337  addsub  8390  addsubeq4  8394  ppncan  8421  leadd1  8610  ltaddsub2  8617  leaddsub2  8619  lemul1  8773  reapmul1lem  8774  reapadd1  8776  reapcotr  8778  remulext1  8779  div23ap  8871  ltmulgt11  9044  lediv1  9049  lemuldiv  9061  zdiv  9568  iooneg  10223  icoshft  10225  fzaddel  10294  fzshftral  10343  facwordi  11003  pfxeq  11281  abssubge0  11680  climshftlemg  11880  dvdsmul1  12392  divalgb  12504  lcmgcdeq  12673  pcfac  12941  mhmmulg  13768  rmodislmodlem  14383  cnmptcom  15041  hmeof1o2  15051