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

Theorem adantrd 484
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 473 . 2 ((𝜓𝜃) → 𝜓)
2 adantrd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 34 1 (𝜑 → ((𝜓𝜃) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  syldan  487  jaoa  532  prlem1  1005  cad0  1555  2eu3  2554  unineq  3875  dfopif  4397  axsep  4778  elssabg  4817  exopxfr2  5264  tz7.7  5747  oneqmini  5774  suctrOLD  5807  fvun1  6267  fconst5  6468  fpropnf1  6521  isomin  6584  isofrlem  6587  poxp  7286  tposfo2  7372  onfununi  7435  tfrlem9a  7479  oecl  7614  oawordri  7627  omwordri  7649  odi  7656  pssnn  8175  prdom2  8826  acni2  8866  cardinfima  8917  cfslb2n  9087  infpssrlem4  9125  axdc3lem4  9272  brdom6disj  9351  tskr1om  9586  indpi  9726  1idpr  9848  1re  10036  mulge0  10543  infm3  10979  uzind  11466  suprfinzcl  11489  uzwo  11748  xrlttr  11970  xmullem2  12092  snunico  12296  fzen  12355  fz0fzelfz0  12441  sqlecan  12966  hashf1lem2  13235  lo1le  14376  fsumss  14450  ntrivcvgfvn0  14625  fprodss  14672  smupvallem  15199  zeqzmulgcd  15226  lcmgcdlem  15313  lcmdvds  15315  lcmfunsnlem2lem1  15345  coprmproddvdslem  15370  cncongr2  15376  exprmfct  15410  infpnlem1  15608  prmdvdsprmop  15741  prmgaplem7  15755  prmlem0  15806  sscfn2  16472  isssc  16474  iszeroi  16653  funcsetcestrclem8  16796  dirge  17231  efgval  18124  dmdprd  18391  dprdw  18403  ringadd2  18569  lpigen  19250  psrbaglefi  19366  matvscl  20231  scmatghm  20333  slesolinv  20480  cpmatacl  20515  pnfnei  21018  mnfnei  21019  cmpcld  21199  isfildlem  21655  metrest  22323  blval2  22361  iscmet3lem2  23084  ivthlem3  23216  mbfi1fseqlem4  23479  itg2seq  23503  dvres  23669  aalioulem6  24086  chpchtsum  24938  dchrmulcl  24968  bcmono  24996  cgrg3col4  25728  brbtwn2  25779  axeuclid  25837  umgredg  26027  pthdivtx  26619  pthdlem1  26656  wwlksext2clwwlk  26917  clwlksfoclwwlk  26956  shsvs  28166  cnlnssadj  28923  atexch  29224  mdsymlem5  29250  disjxpin  29385  sigaclci  30180  poseq  31734  nosupno  31833  nosupbday  31835  nocvxminlem  31877  elfuns  32006  altopth1  32056  btwnexch2  32114  ifscgr  32135  colinbtwnle  32209  trer  32294  elicc3  32295  bj-axsep  32777  bj-finsumval0  33127  poimirlem27  33416  poimir  33422  cnambfre  33438  itg2addnclem2  33442  itg2addnc  33444  areacirclem1  33480  heiborlem4  33593  elghomlem2OLD  33665  rngo2  33686  ispridl2  33817  ispridlc  33849  paddasslem14  34945  ispsubcl2N  35059  cdleme29ex  35488  cdlemefr29exN  35516  eldiophss  37164  rencldnfilem  37210  ioounsn  37621  clsk1indlem3  38167  ntrneikb  38218  ax6e2ndeq  38601  suctrALT2  38898  2reu3  40957  iccpartiltu  41128  bgoldbtbndlem2  41465  rhmsubclem4  41860  elsetrecslem  42215  aacllem  42318
  Copyright terms: Public domain W3C validator