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

Theorem adantrd 495
Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)
Hypothesis
Ref Expression
adantrd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
adantrd (𝜑 → ((𝜓𝜃) → 𝜒))

Proof of Theorem adantrd
StepHypRef Expression
1 simpl 486 . 2 ((𝜓𝜃) → 𝜓)
2 adantrd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 34 1 (𝜑 → ((𝜓𝜃) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  im2anan9  622  jaoa  953  prlem1  1050  cad0  1619  dfsb1  2512  unineq  4239  dfopif  4784  elssabg  5225  exopxfr2  5702  tz7.7  6204  oneqmini  6229  fvun1  6745  fconst5  6959  fpropnf1  7017  isomin  7083  isofrlem  7086  poxp  7818  tposfo2  7911  onfununi  7974  tfrlem9a  8018  oecl  8158  oawordri  8172  omwordri  8194  odi  8201  pssnn  8733  prdom2  9430  acni2  9470  cardinfima  9521  cfslb2n  9688  infpssrlem4  9726  axdc3lem4  9873  brdom6disj  9952  tskr1om  10187  indpi  10327  1idpr  10449  1re  10639  mulge0  11156  infm3  11596  uzind  12071  suprfinzcl  12094  uzwo  12308  xrlttr  12530  xmullem2  12655  snunico  12866  fzen  12928  fz0fzelfz0  13017  sqlecan  13576  hashf1lem2  13819  ccatsymb  13936  lo1le  15008  fsumss  15082  ntrivcvgfvn0  15255  fprodss  15302  smupvallem  15830  zeqzmulgcd  15857  lcmgcdlem  15948  lcmdvds  15950  lcmfunsnlem2lem1  15980  coprmproddvdslem  16004  cncongr2  16010  exprmfct  16046  infpnlem1  16244  prmdvdsprmop  16377  prmgaplem7  16391  prmlem0  16439  sscfn2  17088  isssc  17090  iszeroi  17269  funcsetcestrclem8  17412  dirge  17847  efgval  18843  dmdprd  19120  dprdw  19132  ringadd2  19328  lpigen  20029  psrbaglefi  20617  matvscl  21043  scmatghm  21145  slesolinv  21292  cpmatacl  21328  pnfnei  21832  mnfnei  21833  cmpcld  22014  isfildlem  22469  metrest  23138  blval2  23176  iscmet3lem2  23903  ivthlem3  24064  mbfi1fseqlem4  24329  itg2seq  24353  aalioulem6  24940  chpchtsum  25810  dchrmulcl  25840  bcmono  25868  cgrg3col4  26654  brbtwn2  26706  axeuclid  26764  umgredg  26938  pthdivtx  27525  pthdlem1  27562  shsvs  29113  cnlnssadj  29870  atexch  30171  mdsymlem5  30197  disjxpin  30353  sigaclci  31452  satfv0  32666  satffunlem2lem1  32712  dmopab3rexdif  32713  poseq  33156  nosupno  33264  nosupbday  33266  nocvxminlem  33308  elfuns  33437  altopth1  33487  btwnexch2  33545  ifscgr  33566  colinbtwnle  33640  trer  33725  elicc3  33726  bj-imdirval3  34548  bj-finsumval0  34649  difunieq  34740  fvineqsneu  34777  fvineqsneq  34778  poimirlem27  35033  poimir  35039  cnambfre  35054  itg2addnclem2  35058  itg2addnc  35060  areacirclem1  35094  heiborlem4  35201  elghomlem2OLD  35273  rngo2  35294  ispridl2  35425  ispridlc  35457  iss2  35710  paddasslem14  37078  ispsubcl2N  37192  cdleme29ex  37619  cdlemefr29exN  37647  eldiophss  39636  rencldnfilem  39682  clsk1indlem3  40670  ntrneikb  40721  mnuop3d  40904  ax6e2ndeq  41190  suctrALT2  41468  2reu3  43597  iccpartiltu  43870  bgoldbtbndlem2  44255  rhmsubclem4  44644  itschlc0xyqsol1  45111  elsetrecslem  45159  aacllem  45260
  Copyright terms: Public domain W3C validator