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

Theorem adantrd 483
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 472 . 2 ((𝜓𝜃) → 𝜓)
2 adantrd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 34 1 (𝜑 → ((𝜓𝜃) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  syldan  486  jaoa  531  prlem1  1025  cad0  1596  2eu3  2584  unineq  3910  dfopif  4430  axsep  4813  elssabg  4849  exopxfr2  5299  tz7.7  5787  oneqmini  5814  suctrOLD  5847  fvun1  6308  fconst5  6512  fpropnf1  6564  isomin  6627  isofrlem  6630  poxp  7334  tposfo2  7420  onfununi  7483  tfrlem9a  7527  oecl  7662  oawordri  7675  omwordri  7697  odi  7704  pssnn  8219  prdom2  8867  acni2  8907  cardinfima  8958  cfslb2n  9128  infpssrlem4  9166  axdc3lem4  9313  brdom6disj  9392  tskr1om  9627  indpi  9767  1idpr  9889  1re  10077  mulge0  10584  infm3  11020  uzind  11507  suprfinzcl  11530  uzwo  11789  xrlttr  12011  xmullem2  12133  snunico  12337  fzen  12396  fz0fzelfz0  12484  sqlecan  13011  hashf1lem2  13278  lo1le  14426  fsumss  14500  ntrivcvgfvn0  14675  fprodss  14722  smupvallem  15252  zeqzmulgcd  15279  lcmgcdlem  15366  lcmdvds  15368  lcmfunsnlem2lem1  15398  coprmproddvdslem  15423  cncongr2  15429  exprmfct  15463  infpnlem1  15661  prmdvdsprmop  15794  prmgaplem7  15808  prmlem0  15859  sscfn2  16525  isssc  16527  iszeroi  16706  funcsetcestrclem8  16849  dirge  17284  efgval  18176  dmdprd  18443  dprdw  18455  ringadd2  18621  lpigen  19304  psrbaglefi  19420  matvscl  20285  scmatghm  20387  slesolinv  20534  cpmatacl  20569  pnfnei  21072  mnfnei  21073  cmpcld  21253  isfildlem  21708  metrest  22376  blval2  22414  iscmet3lem2  23136  ivthlem3  23268  mbfi1fseqlem4  23530  itg2seq  23554  dvres  23720  aalioulem6  24137  chpchtsum  24989  dchrmulcl  25019  bcmono  25047  cgrg3col4  25779  brbtwn2  25830  axeuclid  25888  umgredg  26078  pthdivtx  26681  pthdlem1  26718  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  clwlksfoclwwlk  27050  shsvs  28310  cnlnssadj  29067  atexch  29368  mdsymlem5  29394  disjxpin  29527  sigaclci  30323  poseq  31878  nosupno  31974  nosupbday  31976  nocvxminlem  32018  elfuns  32147  altopth1  32197  btwnexch2  32255  ifscgr  32276  colinbtwnle  32350  trer  32435  elicc3  32436  bj-axsep  32918  bj-finsumval0  33277  poimirlem27  33566  poimir  33572  cnambfre  33588  itg2addnclem2  33592  itg2addnc  33594  areacirclem1  33630  heiborlem4  33743  elghomlem2OLD  33815  rngo2  33836  ispridl2  33967  ispridlc  33999  iss2  34252  paddasslem14  35437  ispsubcl2N  35551  cdleme29ex  35979  cdlemefr29exN  36007  eldiophss  37655  rencldnfilem  37701  ioounsn  38112  clsk1indlem3  38658  ntrneikb  38709  ax6e2ndeq  39092  suctrALT2  39386  2reu3  41509  iccpartiltu  41683  bgoldbtbndlem2  42019  rhmsubclem4  42414  elsetrecslem  42770  aacllem  42875
  Copyright terms: Public domain W3C validator