Theorem 3com12 1269

Description: Commutation in antecedent. Swap 1st and 2nd. (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 1045	. 2 |- ( ( ps /\ ph /\ ch ) <-> ( ph /\ ps /\ ch ) )
2		3exp.1	. 2 |- ( ( ph /\ ps /\ ch ) -> th )
3	1, 2	sylbi 207	1 |- ( ( ps /\ ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  3imp21  1277  3adant2l  1320  3adant2r  1321  brelrng  5355  fresaunres1  6077  fvun2  6270  onfununi  7438  oaword  7629  nnaword  7707  nnmword  7713  ecopovtrn  7850  fpmg  7883  tskord  9602  ltadd2  10141  mul12  10202  add12  10253  addsub  10292  addsubeq4  10296  ppncan  10323  leadd1  10496  ltaddsub2  10503  leaddsub2  10505  ltsub1  10524  ltsub2  10525  div23  10704  ltmul1  10873  ltmulgt11  10883  lediv1  10888  lemuldiv  10903  ltdiv2  10909  zdiv  11447  xltadd1  12086  xltmul1  12122  iooneg  12292  icoshft  12294  fzaddel  12375  fzshftral  12428  modmulmodr  12736  facwordi  13076  abssubge0  14067  climshftlem  14305  dvdsmul1  15003  divalglem8  15123  divalgb  15127  lcmgcdeq  15325  pcfac  15603  mhmmulg  17583  rmodislmodlem  18930  xrsdsreval  19791  cnmptcom  21481  hmeof1o2  21566  ordthmeo  21605  isclmi0  22898  iscvsi  22929  cxplt2  24444  axcontlem8  25851  vcdi  27420  isvciOLD  27435  dipdi  27698  dipsubdi  27704  hvadd12  27892  hvmulcom  27900  his5  27943  bcs3  28040  chj12  28393  spansnmul  28423  homul12  28664  hoaddsub  28675  lnopmul  28826  lnopaddmuli  28832  lnopsubmuli  28834  lnfnaddmuli  28904  leop2  28983  dmdsl3  29174  chirredlem3  29251  atmd2  29259  cdj3lem3  29297  signstfvc  30651  3com12d  32304  cnambfre  33458  sdclem2  33538  addrcom  38679  uun123p1  39036  sineq0ALT  39173  stoweidlem17  40234  sigaras  41044  sigarms  41045