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

Theorem adantrr 470
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 108 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 284 1  |-  ( (
ph  /\  ( ps  /\ 
th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
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 is referenced by:  ad2ant2r  500  ad2ant2lr  501  dn1dc  929  3ad2antr1  1131  xordidc  1362  po2nr  4201  sotricim  4215  fmptco  5554  fvtp1g  5596  dff13  5637  fcof1o  5658  isocnv  5680  isores2  5682  isoini  5687  f1oiso2  5696  acexmidlemab  5736  ovmpodf  5870  offval  5957  xp1st  6031  1stconst  6086  cnvf1olem  6089  f1od2  6100  mpoxopoveq  6105  nnaordi  6372  nnmordi  6380  erinxp  6471  dom2lem  6634  fundmen  6668  mapen  6708  ssenen  6713  fidifsnen  6732  difinfsnlem  6952  fodjum  6986  ltsonq  7174  lt2addnq  7180  lt2mulnq  7181  ltexnqq  7184  prarloclemarch2  7195  enq0sym  7208  genprndl  7297  genprndu  7298  prmuloc  7342  distrlem1prl  7358  distrlem1pru  7359  ltsopr  7372  ltexprlemdisj  7382  ltexprlemfl  7385  ltexprlemfu  7387  addcanprlemu  7391  ltaprg  7395  mulcmpblnrlemg  7516  recexgt0sr  7549  mul4  7862  2addsub  7944  muladd  8114  ltleadd  8176  eqord1  8213  eqord2  8214  divmulap3  8405  divcanap7  8449  divadddivap  8455  lemul2a  8585  lemul12b  8587  ltmuldiv2  8601  ltdivmul  8602  ltdivmul2  8604  ledivmul2  8606  lemuldiv2  8608  lt2msq  8612  cju  8687  zextlt  9111  xrlttr  9549  xrre3  9573  ixxdisj  9654  iooshf  9703  icodisj  9743  iccf1o  9755  expsubap  10309  bcval5  10477  hashfacen  10547  seq3coll  10553  sqrt0rlem  10743  lenegsq  10835  zsumdc  11121  fisum0diag2  11184  ndvdsadd  11555  zssinfcl  11568  lcmdvds  11687  oddpwdclemdc  11778  hashdvds  11824  ennnfonelemex  11854  eltg2  12149  ssnei2  12253  restopnb  12277  txdis1cn  12374  txlm  12375  elbl2ps  12488  elbl2  12489  blininf  12520  xmeter  12532  xmetresbl  12536  bdxmet  12597  metrest  12602  dedekindicc  12707  limcimo  12730
  Copyright terms: Public domain W3C validator