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  944  3ad2antr1  1146  xordidc  1377  po2nr  4231  sotricim  4245  fmptco  5586  fvtp1g  5628  dff13  5669  fcof1o  5690  isocnv  5712  isores2  5714  isoini  5719  f1oiso2  5728  acexmidlemab  5768  ovmpodf  5902  offval  5989  xp1st  6063  1stconst  6118  cnvf1olem  6121  f1od2  6132  mpoxopoveq  6137  nnaordi  6404  nnmordi  6412  erinxp  6503  dom2lem  6666  fundmen  6700  mapen  6740  ssenen  6745  fidifsnen  6764  difinfsnlem  6984  fodjum  7018  cc2lem  7086  ltsonq  7218  lt2addnq  7224  lt2mulnq  7225  ltexnqq  7228  prarloclemarch2  7239  enq0sym  7252  genprndl  7341  genprndu  7342  prmuloc  7386  distrlem1prl  7402  distrlem1pru  7403  ltsopr  7416  ltexprlemdisj  7426  ltexprlemfl  7429  ltexprlemfu  7431  addcanprlemu  7435  ltaprg  7439  mulcmpblnrlemg  7560  recexgt0sr  7593  mul4  7906  2addsub  7988  muladd  8158  ltleadd  8220  eqord1  8257  eqord2  8258  divmulap3  8449  divcanap7  8493  divadddivap  8499  lemul2a  8629  lemul12b  8631  ltmuldiv2  8645  ltdivmul  8646  ltdivmul2  8648  ledivmul2  8650  lemuldiv2  8652  lt2msq  8656  cju  8731  zextlt  9155  xrlttr  9593  xrre3  9617  ixxdisj  9698  iooshf  9747  icodisj  9787  iccf1o  9799  expsubap  10353  bcval5  10521  hashfacen  10591  seq3coll  10597  sqrt0rlem  10787  lenegsq  10879  zsumdc  11165  fisum0diag2  11228  prodmodclem2  11358  ndvdsadd  11639  zssinfcl  11652  lcmdvds  11771  oddpwdclemdc  11862  hashdvds  11908  ennnfonelemex  11938  eltg2  12236  ssnei2  12340  restopnb  12364  txdis1cn  12461  txlm  12462  elbl2ps  12575  elbl2  12576  blininf  12607  xmeter  12619  xmetresbl  12623  bdxmet  12684  metrest  12689  dedekindicc  12794  limcimo  12817
  Copyright terms: Public domain W3C validator