MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantrd Unicode version

Theorem adantrd 454
Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)
Hypothesis
Ref Expression
adantrd.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
adantrd  |-  ( ph  ->  ( ( ps  /\  th )  ->  ch )
)

Proof of Theorem adantrd
StepHypRef Expression
1 simpl 443 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adantrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 28 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  syldan  456  jaoa  496  prlem1  928  cad0  1390  equveli  1941  2eu3  2238  unineq  3432  dfopif  3809  axsep  4156  elssabg  4182  tz7.7  4434  oneqmini  4459  suctr  4491  fvun1  5606  fconst5  5747  fconstfv  5750  isomin  5850  isofrlem  5853  exopxfr2  6200  poxp  6243  tposfo2  6273  onfununi  6374  tfrlem9a  6418  oecl  6552  oawordri  6564  omwordri  6586  odi  6593  pssnn  7097  prdom2  7652  acni2  7689  cardinfima  7740  cfslb2n  7910  infpssrlem4  7948  axdc3lem4  8095  brdom6disj  8173  tskr1om  8405  indpi  8547  1idpr  8669  1re  8853  mulge0  9307  infm3  9729  uzind  10119  uzwo  10297  uzwoOLD  10298  xrlttr  10490  xmullem2  10601  snunico  10779  fzen  10827  sqlecan  11225  hashf1lem2  11410  lo1le  12141  fsumss  12214  smupvallem  12690  exprmfct  12805  infpnlem1  12973  prmlem0  13123  sscfn2  13711  isssc  13713  dirge  14375  efgval  15042  dmdprd  15252  dprdw  15261  lpigen  16024  psrbaglefi  16134  pnfnei  16966  mnfnei  16967  cmpcld  17145  isfildlem  17568  metrest  18086  iscmet3lem2  18734  ivthlem3  18829  mbfi1fseqlem4  19089  itg2seq  19113  dvres  19277  aalioulem6  19733  chpchtsum  20474  dchrmulcl  20504  bcmono  20532  elghomlem2  21045  rngo2  21071  shsvs  21918  cnlnssadj  22676  atexch  22977  mdsymlem5  23003  sigaclci  23508  poseq  24324  nocvxminlem  24415  nofulllem5  24431  altopth1  24571  brbtwn2  24605  axeuclid  24663  btwnexch2  24718  ifscgr  24739  colinbtwnle  24813  itg2addnclem2  25004  itg2addnc  25005  areacirclem2  25028  ridlideq  25438  intcont  25646  limptlimpr2lem1  25677  islimrs3  25684  islimrs4  25685  distsava  25792  cmpmon  25918  iepiclem  25926  setiscat  26082  clscnc  26113  trer  26330  elicc3  26331  heiborlem4  26641  ispridl2  26766  ispridlc  26798  eldiophss  26957  rencldnfilem  27006  2reu3  28069  opabbrex  28191  usgraedgprv  28256  4cycl4dv  28413  a9e2ndeq  28624  suctrALT2  28929  equveliNEW7  29503  paddasslem14  30644  ispsubcl2N  30758  cdleme29ex  31185  cdlemefr29exN  31213
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator