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  7852  prcunqu  7853  prarloc  7871  ltaprg  7987  mul12  8457  add12  8486  addsub  8539  addsubeq4  8543  ppncan  8570  leadd1  8760  ltaddsub2  8767  leaddsub2  8769  lemul1  8924  reapmul1lem  8925  reapadd1  8927  reapcotr  8929  remulext1  8930  div23ap  9024  ltmulgt11  9197  lediv1  9202  lemuldiv  9214  zdiv  9739  iooneg  10401  icoshft  10403  fzaddel  10476  fzshftral  10526  facwordi  11194  pfxeq  11484  abssubge0  11885  climshftlemg  12087  dvdsmul1  12599  divalgb  12711  lcmgcdeq  12880  pcfac  13152  mhmmulg  14019  rmodislmodlem  14771  cnmptcom  15490  hmeof1o2  15500