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

Theorem 3com12 1202
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 980 . 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 973
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 975
This theorem is referenced by:  3adant2l  1227  3adant2r  1228  brelrng  4842  iotam  5190  funimaexglem  5281  fvun2  5563  nnaordi  6487  nnmword  6497  fpmg  6652  prcdnql  7446  prcunqu  7447  prarloc  7465  ltaprg  7581  mul12  8048  add12  8077  addsub  8130  addsubeq4  8134  ppncan  8161  leadd1  8349  ltaddsub2  8356  leaddsub2  8358  lemul1  8512  reapmul1lem  8513  reapadd1  8515  reapcotr  8517  remulext1  8518  div23ap  8608  ltmulgt11  8780  lediv1  8785  lemuldiv  8797  zdiv  9300  iooneg  9945  icoshft  9947  fzaddel  10015  fzshftral  10064  facwordi  10674  abssubge0  11066  climshftlemg  11265  dvdsmul1  11775  divalgb  11884  lcmgcdeq  12037  pcfac  12302  cnmptcom  13092  hmeof1o2  13102
  Copyright terms: Public domain W3C validator