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  6785  nnmword  6795  fpmg  6959  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  9745  iooneg  10407  icoshft  10409  fzaddel  10482  fzshftral  10532  facwordi  11200  pfxeq  11490  abssubge0  11891  climshftlemg  12093  dvdsmul1  12605  divalgb  12717  lcmgcdeq  12886  pcfac  13158  mhmmulg  14025  rmodislmodlem  14796  cnmptcom  15524  hmeof1o2  15534