Theorem 3com12 1234

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 1012	. 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 )

Syntax hints:   -> wi 4   /\ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  3adant2l  1259  3adant2r  1260  brelrng  4990  iotam  5346  funimaexglem  5441  fresaunres1disj  5548  fvun2  5746  nnaordi  6743  nnmword  6753  fpmg  6910  prcdnql  7801  prcunqu  7802  prarloc  7820  ltaprg  7936  mul12  8404  add12  8433  addsub  8486  addsubeq4  8490  ppncan  8517  leadd1  8706  ltaddsub2  8713  leaddsub2  8715  lemul1  8869  reapmul1lem  8870  reapadd1  8872  reapcotr  8874  remulext1  8875  div23ap  8967  ltmulgt11  9140  lediv1  9145  lemuldiv  9157  zdiv  9669  iooneg  10324  icoshft  10326  fzaddel  10396  fzshftral  10446  facwordi  11106  pfxeq  11392  abssubge0  11791  climshftlemg  11991  dvdsmul1  12503  divalgb  12615  lcmgcdeq  12784  pcfac  13052  mhmmulg  13897  rmodislmodlem  14515  cnmptcom  15180  hmeof1o2  15190