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

Theorem 3com12 1207
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 985 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ph  /\  ps  /\  ch ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2sylbi 121 1  |-  ( ( ps  /\  ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  3adant2l  1232  3adant2r  1233  brelrng  4860  iotam  5210  funimaexglem  5301  fvun2  5585  nnaordi  6511  nnmword  6521  fpmg  6676  prcdnql  7485  prcunqu  7486  prarloc  7504  ltaprg  7620  mul12  8088  add12  8117  addsub  8170  addsubeq4  8174  ppncan  8201  leadd1  8389  ltaddsub2  8396  leaddsub2  8398  lemul1  8552  reapmul1lem  8553  reapadd1  8555  reapcotr  8557  remulext1  8558  div23ap  8650  ltmulgt11  8823  lediv1  8828  lemuldiv  8840  zdiv  9343  iooneg  9990  icoshft  9992  fzaddel  10061  fzshftral  10110  facwordi  10722  abssubge0  11113  climshftlemg  11312  dvdsmul1  11822  divalgb  11932  lcmgcdeq  12085  pcfac  12350  mhmmulg  13029  rmodislmodlem  13445  cnmptcom  13837  hmeof1o2  13847
  Copyright terms: Public domain W3C validator