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

Theorem adantrd 492
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 483 . 2 ((𝜓𝜃) → 𝜓)
2 adantrd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 34 1 (𝜑 → ((𝜓𝜃) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  im2anan9  619  jaoa  949  prlem1  1046  cad0  1609  dfsb1  2503  2eu3OLD  2733  unineq  4251  dfopif  4792  elssabg  5230  exopxfr2  5708  tz7.7  6210  oneqmini  6235  fvun1  6747  fconst5  6960  fpropnf1  7016  isomin  7079  isofrlem  7082  poxp  7811  tposfo2  7904  onfununi  7967  tfrlem9a  8011  oecl  8151  oawordri  8165  omwordri  8187  odi  8194  pssnn  8724  prdom2  9420  acni2  9460  cardinfima  9511  cfslb2n  9678  infpssrlem4  9716  axdc3lem4  9863  brdom6disj  9942  tskr1om  10177  indpi  10317  1idpr  10439  1re  10629  mulge0  11146  infm3  11588  uzind  12062  suprfinzcl  12085  uzwo  12299  xrlttr  12521  xmullem2  12646  snunico  12853  fzen  12912  fz0fzelfz0  13001  sqlecan  13559  hashf1lem2  13802  ccatsymb  13924  lo1le  14996  fsumss  15070  ntrivcvgfvn0  15243  fprodss  15290  smupvallem  15820  zeqzmulgcd  15847  lcmgcdlem  15938  lcmdvds  15940  lcmfunsnlem2lem1  15970  coprmproddvdslem  15994  cncongr2  16000  exprmfct  16036  infpnlem1  16234  prmdvdsprmop  16367  prmgaplem7  16381  prmlem0  16427  sscfn2  17076  isssc  17078  iszeroi  17257  funcsetcestrclem8  17400  dirge  17835  efgval  18772  dmdprd  19049  dprdw  19061  ringadd2  19254  lpigen  19957  psrbaglefi  20080  matvscl  20968  scmatghm  21070  slesolinv  21217  cpmatacl  21252  pnfnei  21756  mnfnei  21757  cmpcld  21938  isfildlem  22393  metrest  23061  blval2  23099  iscmet3lem2  23822  ivthlem3  23981  mbfi1fseqlem4  24246  itg2seq  24270  aalioulem6  24853  chpchtsum  25722  dchrmulcl  25752  bcmono  25780  cgrg3col4  26566  brbtwn2  26618  axeuclid  26676  umgredg  26850  pthdivtx  27437  pthdlem1  27474  shsvs  29027  cnlnssadj  29784  atexch  30085  mdsymlem5  30111  disjxpin  30266  sigaclci  31290  satfv0  32502  satffunlem2lem1  32548  dmopab3rexdif  32549  poseq  32992  nosupno  33100  nosupbday  33102  nocvxminlem  33144  elfuns  33273  altopth1  33323  btwnexch2  33381  ifscgr  33402  colinbtwnle  33476  trer  33561  elicc3  33562  bj-imdirval3  34366  bj-finsumval0  34455  difunieq  34537  fvineqsneu  34574  fvineqsneq  34575  poimirlem27  34800  poimir  34806  cnambfre  34821  itg2addnclem2  34825  itg2addnc  34827  areacirclem1  34863  heiborlem4  34973  elghomlem2OLD  35045  rngo2  35066  ispridl2  35197  ispridlc  35229  iss2  35482  paddasslem14  36849  ispsubcl2N  36963  cdleme29ex  37390  cdlemefr29exN  37418  eldiophss  39249  rencldnfilem  39295  clsk1indlem3  40271  ntrneikb  40322  mnuop3d  40484  ax6e2ndeq  40770  suctrALT2  41048  2reu3  43186  iccpartiltu  43459  bgoldbtbndlem2  43848  rhmsubclem4  44288  itschlc0xyqsol1  44681  elsetrecslem  44729  aacllem  44830
  Copyright terms: Public domain W3C validator