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

Theorem 3com12 1168
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 952 . 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 945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  3adant2l  1193  3adant2r  1194  brelrng  4730  funimaexglem  5164  fvun2  5442  nnaordi  6358  nnmword  6368  fpmg  6522  prcdnql  7240  prcunqu  7241  prarloc  7259  ltaprg  7375  mul12  7814  add12  7843  addsub  7896  addsubeq4  7900  ppncan  7927  leadd1  8111  ltaddsub2  8118  leaddsub2  8120  lemul1  8273  reapmul1lem  8274  reapadd1  8276  reapcotr  8278  remulext1  8279  div23ap  8364  ltmulgt11  8532  lediv1  8537  lemuldiv  8549  zdiv  9043  iooneg  9664  icoshft  9666  fzaddel  9732  fzshftral  9781  facwordi  10379  abssubge0  10766  climshftlemg  10963  dvdsmul1  11363  divalgb  11470  lcmgcdeq  11610  cnmptcom  12309
  Copyright terms: Public domain W3C validator