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  5015  iotam  5372  funimaexglem  5467  fresaunres1disj  5574  fvun2  5773  nnaordi  6786  nnmword  6796  fpmg  6960  prcdnql  7857  prcunqu  7858  prarloc  7876  ltaprg  7992  mul12  8462  add12  8491  addsub  8544  addsubeq4  8548  ppncan  8575  leadd1  8765  ltaddsub2  8772  leaddsub2  8774  lemul1  8929  reapmul1lem  8930  reapadd1  8932  reapcotr  8934  remulext1  8935  div23ap  9029  ltmulgt11  9202  lediv1  9207  lemuldiv  9219  zdiv  9744  iooneg  10406  icoshft  10408  fzaddel  10481  fzshftral  10531  facwordi  11199  pfxeq  11489  abssubge0  11890  climshftlemg  12092  dvdsmul1  12604  divalgb  12716  lcmgcdeq  12885  pcfac  13157  mhmmulg  14024  rmodislmodlem  14795  cnmptcom  15541  hmeof1o2  15551