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

Step	Hyp	Ref	Expression
1		simpl 483	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adantrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

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 206  df-an 397

This theorem is referenced by:  im2anan9  620  jaoa  953  prlem1  1052  cad0  1620  cad0OLD  1621  dfsb1  2485  unineq  4211  dfopifOLD  4801  elssabg  5260  exopxfr2  5753  tz7.7  6292  oneqmini  6317  fvun1  6859  fconst5  7081  fpropnf1  7140  isomin  7208  isofrlem  7211  poxp  7969  tposfo2  8065  onfununi  8172  tfrlem9a  8217  oecl  8367  oawordri  8381  omwordri  8403  odi  8410  pssnn  8951  pssnnOLD  9040  prdom2  9762  acni2  9802  cardinfima  9853  cfslb2n  10024  infpssrlem4  10062  axdc3lem4  10209  brdom6disj  10288  tskr1om  10523  indpi  10663  1idpr  10785  1re  10975  mulge0  11493  infm3  11934  uzind  12412  suprfinzcl  12436  uzwo  12651  xrlttr  12874  xmullem2  12999  snunico  13211  fzen  13273  fz0fzelfz0  13362  sqlecan  13925  hashf1lem2  14170  ccatsymb  14287  lo1le  15363  fsumss  15437  ntrivcvgfvn0  15611  fprodss  15658  smupvallem  16190  zeqzmulgcd  16217  lcmgcdlem  16311  lcmdvds  16313  lcmfunsnlem2lem1  16343  coprmproddvdslem  16367  cncongr2  16373  exprmfct  16409  infpnlem1  16611  prmdvdsprmop  16744  prmgaplem7  16758  prmlem0  16807  sscfn2  17530  isssc  17532  iszeroi  17724  funcsetcestrclem8  17879  dirge  18321  efgval  19323  dmdprd  19601  dprdw  19613  ringadd2  19814  lpigen  20527  psrbaglefi  21135  psrbaglefiOLD  21136  matvscl  21580  scmatghm  21682  slesolinv  21829  cpmatacl  21865  pnfnei  22371  mnfnei  22372  cmpcld  22553  isfildlem  23008  metrest  23680  blval2  23718  iscmet3lem2  24456  ivthlem3  24617  mbfi1fseqlem4  24883  itg2seq  24907  aalioulem6  25497  chpchtsum  26367  dchrmulcl  26397  bcmono  26425  cgrg3col4  27214  brbtwn2  27273  axeuclid  27331  umgredg  27508  pthdivtx  28097  pthdlem1  28134  shsvs  29685  cnlnssadj  30442  atexch  30743  mdsymlem5  30769  disjxpin  30927  sigaclci  32100  fnrelpredd  33061  satfv0  33320  satffunlem2lem1  33366  dmopab3rexdif  33367  poseq  33802  nosupno  33906  nosupbday  33908  noinfno  33921  noinfbday  33923  nocvxminlem  33972  elfuns  34217  altopth1  34267  btwnexch2  34325  ifscgr  34346  colinbtwnle  34420  trer  34505  elicc3  34506  bj-imdirval3  35355  bj-finsumval0  35456  difunieq  35545  fvineqsneu  35582  fvineqsneq  35583  poimirlem27  35804  poimir  35810  cnambfre  35825  itg2addnclem2  35829  itg2addnc  35831  areacirclem1  35865  heiborlem4  35972  elghomlem2OLD  36044  rngo2  36065  ispridl2  36196  ispridlc  36228  iss2  36479  paddasslem14  37847  ispsubcl2N  37961  cdleme29ex  38388  cdlemefr29exN  38416  eldiophss  40596  rencldnfilem  40642  clsk1indlem3  41653  ntrneikb  41704  mnuop3d  41889  ax6e2ndeq  42179  suctrALT2  42457  2reu3  44602  iccpartiltu  44874  bgoldbtbndlem2  45258  rhmsubclem4  45647  itschlc0xyqsol1  46112  elsetrecslem  46404  aacllem  46505