Theorem 3com12 1238

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 1016	. 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 1009

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 1011

This theorem is referenced by:  3adant2l  1263  3adant2r  1264  brelrng  5008  iotam  5364  funimaexglem  5459  fresaunres1disj  5566  fvun2  5764  nnaordi  6771  nnmword  6781  fpmg  6945  prcdnql  7841  prcunqu  7842  prarloc  7860  ltaprg  7976  mul12  8445  add12  8474  addsub  8527  addsubeq4  8531  ppncan  8558  leadd1  8748  ltaddsub2  8755  leaddsub2  8757  lemul1  8911  reapmul1lem  8912  reapadd1  8914  reapcotr  8916  remulext1  8917  div23ap  9011  ltmulgt11  9184  lediv1  9189  lemuldiv  9201  zdiv  9713  iooneg  10369  icoshft  10371  fzaddel  10443  fzshftral  10493  facwordi  11156  pfxeq  11446  abssubge0  11846  climshftlemg  12046  dvdsmul1  12558  divalgb  12670  lcmgcdeq  12839  pcfac  13107  mhmmulg  13943  rmodislmodlem  14659  cnmptcom  15322  hmeof1o2  15332