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

Theorem adantrd 482
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 471 . 2 ((𝜓𝜃) → 𝜓)
2 adantrd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 33 1 (𝜑 → ((𝜓𝜃) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  syldan  485  jaoa  530  prlem1  996  cad0  1546  19.40bOLD  1804  2eu3  2539  unineq  3832  dfopif  4328  axsep  4699  elssabg  4738  exopxfr2  5173  tz7.7  5649  oneqmini  5676  suctrOLD  5709  fvun1  6161  fconst5  6351  isomin  6462  isofrlem  6465  poxp  7150  tposfo2  7236  onfununi  7299  tfrlem9a  7343  oecl  7478  oawordri  7491  omwordri  7513  odi  7520  pssnn  8037  prdom2  8686  acni2  8726  cardinfima  8777  cfslb2n  8947  infpssrlem4  8985  axdc3lem4  9132  brdom6disj  9209  tskr1om  9442  indpi  9582  1idpr  9704  1re  9892  mulge0  10392  infm3  10828  uzind  11298  suprfinzcl  11321  uzwo  11580  xrlttr  11805  xmullem2  11921  snunico  12123  fzen  12181  fz0fzelfz0  12266  sqlecan  12785  hashf1lem2  13046  lo1le  14173  fsumss  14246  ntrivcvgfvn0  14413  fprodss  14460  smupvallem  14986  zeqzmulgcd  15013  lcmgcdlem  15100  lcmdvds  15102  lcmfunsnlem2lem1  15132  coprmproddvdslem  15157  cncongr2  15163  exprmfct  15197  infpnlem1  15395  prmdvdsprmop  15528  prmgaplem7  15542  prmlem0  15593  sscfn2  16244  isssc  16246  iszeroi  16425  funcsetcestrclem8  16568  dirge  17003  efgval  17896  dmdprd  18163  dprdw  18175  ringadd2  18341  lpigen  19020  psrbaglefi  19136  matvscl  19995  scmatghm  20097  slesolinv  20244  cpmatacl  20279  pnfnei  20773  mnfnei  20774  cmpcld  20954  isfildlem  21410  metrest  22077  blval2  22115  iscmet3lem2  22813  ivthlem3  22943  mbfi1fseqlem4  23205  itg2seq  23229  dvres  23395  aalioulem6  23810  chpchtsum  24658  dchrmulcl  24688  bcmono  24716  cgrg3col4  25449  brbtwn2  25500  axeuclid  25558  usgraedgprv  25668  usgranloopv  25670  4cycl4dv  25958  0clwlk  26056  wwlkext2clwwlk  26094  frg2wot1  26347  numclwwlkun  26369  shsvs  27369  cnlnssadj  28126  atexch  28427  mdsymlem5  28453  disjxpin  28586  sigaclci  29325  poseq  30797  nocvxminlem  30892  nofulllem5  30908  elfuns  30995  altopth1  31045  btwnexch2  31103  ifscgr  31124  colinbtwnle  31198  trer  31283  elicc3  31284  bj-axsep  31791  bj-finsumval0  32124  poimirlem27  32406  poimir  32412  cnambfre  32428  itg2addnclem2  32432  itg2addnc  32434  areacirclem1  32470  heiborlem4  32583  elghomlem2OLD  32655  rngo2  32676  ispridl2  32807  ispridlc  32839  paddasslem14  33937  ispsubcl2N  34051  cdleme29ex  34480  cdlemefr29exN  34508  eldiophss  36156  rencldnfilem  36202  ioounsn  36614  clsk1indlem3  37161  ntrneikb  37212  ax6e2ndeq  37596  suctrALT2  37894  2reu3  39638  iccpartiltu  39762  bgoldbtbndlem2  40024  fpropnf1  40161  umgredg  40370  pthdivtx  40934  pthdlem1  40971  wwlksext2clwwlk  41230  clwlksfoclwwlk  41269  frgr2wwlk1  41493  fusgr2wsp2nb  41497  rhmsubclem4  41880  aacllem  42316
  Copyright terms: Public domain W3C validator