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

Theorem 3com12 1143
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 927 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ph  /\  ps  /\  ch ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2sylbi 119 1  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  3adant2l  1164  3adant2r  1165  brelrng  4613  funimaexglem  5033  fvun2  5292  nnaordi  6168  nnmword  6178  prcdnql  6788  prcunqu  6789  prarloc  6807  ltaprg  6923  mul12  7356  add12  7385  addsub  7438  addsubeq4  7442  ppncan  7469  leadd1  7653  ltaddsub2  7660  leaddsub2  7662  lemul1  7812  reapmul1lem  7813  reapadd1  7815  reapcotr  7817  remulext1  7818  div23ap  7898  ltmulgt11  8061  lediv1  8066  lemuldiv  8078  zdiv  8568  iooneg  9138  icoshft  9140  fzaddel  9205  fzshftral  9253  facwordi  9816  abssubge0  10189  climshftlemg  10342  dvdsmul1  10425  divalgb  10532  lcmgcdeq  10672
  Copyright terms: Public domain W3C validator