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

Theorem 3com12 1147
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 931 . 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 924
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 926
This theorem is referenced by:  3adant2l  1168  3adant2r  1169  brelrng  4654  funimaexglem  5083  fvun2  5355  nnaordi  6247  nnmword  6257  fpmg  6411  prcdnql  7022  prcunqu  7023  prarloc  7041  ltaprg  7157  mul12  7590  add12  7619  addsub  7672  addsubeq4  7676  ppncan  7703  leadd1  7887  ltaddsub2  7894  leaddsub2  7896  lemul1  8046  reapmul1lem  8047  reapadd1  8049  reapcotr  8051  remulext1  8052  div23ap  8132  ltmulgt11  8297  lediv1  8302  lemuldiv  8314  zdiv  8804  iooneg  9374  icoshft  9376  fzaddel  9441  fzshftral  9489  facwordi  10113  abssubge0  10500  climshftlemg  10654  dvdsmul1  10911  divalgb  11018  lcmgcdeq  11158
  Copyright terms: Public domain W3C validator