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

Theorem adantrd 456
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 445 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adantrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 31 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  syldan  458  jaoa  498  prlem1  930  cad0  1410  equveliOLD  2087  2eu3  2365  unineq  3593  dfopif  3983  axsep  4331  elssabg  4357  tz7.7  4609  oneqmini  4634  suctrALT  4666  fvun1  5796  fconst5  5951  fconstfv  5956  isomin  6059  isofrlem  6062  opabbrex  6120  exopxfr2  6413  poxp  6460  tposfo2  6504  onfununi  6605  tfrlem9a  6649  oecl  6783  oawordri  6795  omwordri  6817  odi  6824  pssnn  7329  prdom2  7892  acni2  7929  cardinfima  7980  cfslb2n  8150  infpssrlem4  8188  axdc3lem4  8335  brdom6disj  8412  tskr1om  8644  indpi  8786  1idpr  8908  1re  9092  mulge0  9547  infm3  9969  uzind  10363  uzwo  10541  uzwoOLD  10542  xrlttr  10735  xmullem2  10846  snunico  11026  fzen  11074  sqlecan  11489  hashf1lem2  11707  lo1le  12447  fsumss  12521  smupvallem  12997  exprmfct  13112  infpnlem1  13280  prmlem0  13430  sscfn2  14020  isssc  14022  dirge  14684  efgval  15351  dmdprd  15561  dprdw  15570  lpigen  16329  psrbaglefi  16439  pnfnei  17286  mnfnei  17287  cmpcld  17467  isfildlem  17891  metrest  18556  blval2  18607  iscmet3lem2  19247  ivthlem3  19352  mbfi1fseqlem4  19612  itg2seq  19636  dvres  19800  aalioulem6  20256  chpchtsum  21005  dchrmulcl  21035  bcmono  21063  usgraedgprv  21398  usgranloopv  21400  4cycl4dv  21656  elghomlem2  21952  rngo2  21978  shsvs  22827  cnlnssadj  23585  atexch  23886  mdsymlem5  23912  disjxpin  24030  sigaclci  24517  ntrivcvgfvn0  25229  fprodss  25276  poseq  25530  nocvxminlem  25647  nofulllem5  25663  elfuns  25762  altopth1  25812  brbtwn2  25846  axeuclid  25904  btwnexch2  25959  ifscgr  25980  colinbtwnle  26054  cnambfre  26257  itg2addnclem2  26259  itg2addnc  26261  areacirclem1  26294  trer  26321  elicc3  26322  heiborlem4  26525  ispridl2  26650  ispridlc  26682  eldiophss  26835  rencldnfilem  26883  2reu3  27944  fz0fzelfz0  28129  swrdtrcfv0  28217  swrdtrcfvl  28287  frg2wot1  28508  a9e2ndeq  28708  suctrALT2  29011  equveliNEW7  29590  paddasslem14  30692  ispsubcl2N  30806  cdleme29ex  31233  cdlemefr29exN  31261
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 179  df-an 362
  Copyright terms: Public domain W3C validator