ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3com12 Unicode version

Theorem 3com12 1189
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
StepHypRef Expression
1 3ancoma 970 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ph  /\  ps  /\  ch ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2sylbi 120 1  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  3adant2l  1214  3adant2r  1215  brelrng  4819  funimaexglem  5255  fvun2  5537  nnaordi  6457  nnmword  6467  fpmg  6621  prcdnql  7406  prcunqu  7407  prarloc  7425  ltaprg  7541  mul12  8008  add12  8037  addsub  8090  addsubeq4  8094  ppncan  8121  leadd1  8309  ltaddsub2  8316  leaddsub2  8318  lemul1  8472  reapmul1lem  8473  reapadd1  8475  reapcotr  8477  remulext1  8478  div23ap  8568  ltmulgt11  8740  lediv1  8745  lemuldiv  8757  zdiv  9257  iooneg  9898  icoshft  9900  fzaddel  9967  fzshftral  10016  facwordi  10625  abssubge0  11013  climshftlemg  11210  dvdsmul1  11720  divalgb  11828  lcmgcdeq  11975  cnmptcom  12768  hmeof1o2  12778
  Copyright terms: Public domain W3C validator