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

Theorem adantrr 456
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
adantrr  |-  ( (
ph  /\  ( ps  /\ 
th ) )  ->  ch )

Proof of Theorem adantrr
StepHypRef Expression
1 simpl 106 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 274 1  |-  ( (
ph  /\  ( ps  /\ 
th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  ad2ant2r  486  ad2ant2lr  487  dn1dc  878  3ad2antr1  1080  xordidc  1306  po2nr  4073  sotricim  4087  fmptco  5357  fvtp1g  5396  dff13  5434  fcof1o  5456  isocnv  5478  isores2  5480  isoini  5484  f1oiso2  5493  acexmidlemab  5533  ovmpt2df  5659  offval  5746  xp1st  5819  1stconst  5869  cnvf1olem  5872  f1od2  5883  mpt2xopoveq  5885  nnaordi  6111  nnmordi  6119  erinxp  6210  dom2lem  6282  fundmen  6316  fidifsnen  6361  ltsonq  6553  lt2addnq  6559  lt2mulnq  6560  ltexnqq  6563  prarloclemarch2  6574  enq0sym  6587  genprndl  6676  genprndu  6677  prmuloc  6721  distrlem1prl  6737  distrlem1pru  6738  ltsopr  6751  ltexprlemdisj  6761  ltexprlemfl  6764  ltexprlemfu  6766  addcanprlemu  6770  ltaprg  6774  mulcmpblnrlemg  6882  recexgt0sr  6915  mul4  7205  2addsub  7287  muladd  7452  ltleadd  7514  divmulap3  7729  divcanap7  7771  divadddivap  7777  lemul2a  7899  lemul12b  7901  ltmuldiv2  7915  ltdivmul  7916  ltdivmul2  7918  ledivmul2  7920  lemuldiv2  7922  lt2msq  7926  cju  7988  zextlt  8389  xrlttr  8816  xrre3  8835  ixxdisj  8872  iooshf  8921  icodisj  8960  iccf1o  8972  expsubap  9462  ibcval5  9624  sqrt0rlem  9822  lenegsq  9914  oddpwdclemdc  10233
  Copyright terms: Public domain W3C validator