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

Theorem adantrr 463
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 107 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 280 1  |-  ( (
ph  /\  ( ps  /\ 
th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
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 is referenced by:  ad2ant2r  493  ad2ant2lr  494  dn1dc  902  3ad2antr1  1104  xordidc  1331  po2nr  4092  sotricim  4106  fmptco  5382  fvtp1g  5421  dff13  5459  fcof1o  5480  isocnv  5502  isores2  5504  isoini  5508  f1oiso2  5517  acexmidlemab  5557  ovmpt2df  5683  offval  5770  xp1st  5843  1stconst  5893  cnvf1olem  5896  f1od2  5907  mpt2xopoveq  5909  nnaordi  6168  nnmordi  6176  erinxp  6267  dom2lem  6340  fundmen  6374  fidifsnen  6426  ltsonq  6702  lt2addnq  6708  lt2mulnq  6709  ltexnqq  6712  prarloclemarch2  6723  enq0sym  6736  genprndl  6825  genprndu  6826  prmuloc  6870  distrlem1prl  6886  distrlem1pru  6887  ltsopr  6900  ltexprlemdisj  6910  ltexprlemfl  6913  ltexprlemfu  6915  addcanprlemu  6919  ltaprg  6923  mulcmpblnrlemg  7031  recexgt0sr  7064  mul4  7359  2addsub  7441  muladd  7607  ltleadd  7669  divmulap3  7884  divcanap7  7928  divadddivap  7934  lemul2a  8056  lemul12b  8058  ltmuldiv2  8072  ltdivmul  8073  ltdivmul2  8075  ledivmul2  8077  lemuldiv2  8079  lt2msq  8083  cju  8157  zextlt  8572  xrlttr  8998  xrre3  9017  ixxdisj  9054  iooshf  9103  icodisj  9142  iccf1o  9154  expsubap  9673  ibcval5  9839  sqrt0rlem  10090  lenegsq  10182  ndvdsadd  10538  zssinfcl  10551  lcmdvds  10668  oddpwdclemdc  10758  hashdvds  10804
  Copyright terms: Public domain W3C validator