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 )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3adant2l  1263  3adant2r  1264  brelrng  5013  iotam  5369  funimaexglem  5464  fresaunres1disj  5571  fvun2  5770  nnaordi  6781  nnmword  6791  fpmg  6955  prcdnql  7851  prcunqu  7852  prarloc  7870  ltaprg  7986  mul12  8456  add12  8485  addsub  8538  addsubeq4  8542  ppncan  8569  leadd1  8759  ltaddsub2  8766  leaddsub2  8768  lemul1  8923  reapmul1lem  8924  reapadd1  8926  reapcotr  8928  remulext1  8929  div23ap  9023  ltmulgt11  9196  lediv1  9201  lemuldiv  9213  zdiv  9738  iooneg  10400  icoshft  10402  fzaddel  10475  fzshftral  10525  facwordi  11192  pfxeq  11482  abssubge0  11883  climshftlemg  12084  dvdsmul1  12596  divalgb  12708  lcmgcdeq  12877  pcfac  13149  mhmmulg  14015  rmodislmodlem  14736  cnmptcom  15448  hmeof1o2  15458