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

Theorem adantrd 468
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 457 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adantrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 32 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  syldan  470  jaoa  510  prlem1  953  cad0  1442  2eu3  2367  unineq  3621  dfopif  4077  axsep  4433  elssabg  4468  tz7.7  4766  oneqmini  4791  suctr  4823  exopxfr2  5005  fvun1  5783  fconst5  5956  fconstfv  5961  isomin  6049  isofrlem  6052  opabbrex  6151  poxp  6705  tposfo2  6789  onfununi  6823  tfrlem9a  6866  oecl  6998  oawordri  7010  omwordri  7032  odi  7039  pssnn  7552  prdom2  8194  acni2  8237  cardinfima  8288  cfslb2n  8458  infpssrlem4  8496  axdc3lem4  8643  brdom6disj  8720  tskr1om  8955  indpi  9097  1idpr  9219  1re  9406  mulge0  9878  infm3  10310  uzind  10754  uzwo  10938  uzwoOLD  10939  xrlttr  11138  xmullem2  11249  snunico  11433  fzen  11488  fz0fzelfz0  11507  sqlecan  11993  hashf1lem2  12230  lo1le  13150  fsumss  13223  smupvallem  13700  exprmfct  13817  infpnlem1  13992  prmlem0  14154  sscfn2  14752  isssc  14754  dirge  15428  efgval  16235  dmdprd  16502  dprdw  16516  dprdwOLD  16522  lpigen  17360  psrbaglefi  17463  psrbaglefiOLD  17464  slesolinv  18508  pnfnei  18846  mnfnei  18847  cmpcld  19027  isfildlem  19452  metrest  20121  blval2  20172  iscmet3lem2  20825  ivthlem3  20959  mbfi1fseqlem4  21218  itg2seq  21242  dvres  21408  aalioulem6  21825  chpchtsum  22580  dchrmulcl  22610  bcmono  22638  brbtwn2  23173  axeuclid  23231  usgraedgprv  23317  usgranloopv  23319  4cycl4dv  23575  elghomlem2  23871  rngo2  23897  shsvs  24748  cnlnssadj  25506  atexch  25807  mdsymlem5  25833  disjxpin  25952  sigaclci  26597  ntrivcvgfvn0  27436  fprodss  27483  poseq  27736  nocvxminlem  27853  nofulllem5  27869  elfuns  27968  altopth1  28018  btwnexch2  28076  ifscgr  28097  colinbtwnle  28171  cnambfre  28466  itg2addnclem2  28470  itg2addnc  28472  areacirclem1  28510  trer  28537  elicc3  28538  heiborlem4  28739  ispridl2  28864  ispridlc  28896  eldiophss  29139  rencldnfilem  29185  ioounsn  29611  2reu3  30038  0clwlk  30454  wwlkext2clwwlk  30491  frg2wot1  30676  suprfinzcl  30774  scmatmulcl  30925  cnstpmatacl  31068  ax6e2ndeq  31364  suctrALT2  31669  bj-dfif5ALT  32182  bj-19.40b  32258  bj-axsep  32410  bj-finsumval0  32679  paddasslem14  33573  ispsubcl2N  33687  cdleme29ex  34114  cdlemefr29exN  34142
  Copyright terms: Public domain W3C validator