Theorem adantrd 491

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 482	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adantrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  im2anan9  619  jaoa  956  prlem1  1055  cad0  1615  cad0OLD  1616  dfsb1  2489  unineq  4307  dfopif  4894  elssabg  5361  exopxfr2  5869  tz7.7  6421  oneqmini  6447  fvun1  7013  fconst5  7243  fpropnf1  7304  isomin  7373  isofrlem  7376  poxp  8169  poseq  8199  tposfo2  8290  onfununi  8397  tfrlem9a  8442  oecl  8593  oawordri  8606  omwordri  8628  odi  8635  pssnn  9234  prdom2  10075  acni2  10115  cardinfima  10166  cfslb2n  10337  infpssrlem4  10375  axdc3lem4  10522  brdom6disj  10601  tskr1om  10836  indpi  10976  1idpr  11098  1re  11290  mulge0  11808  infm3  12254  uzind  12735  suprfinzcl  12757  uzwo  12976  xrlttr  13202  xmullem2  13327  snunico  13539  fzen  13601  fz0fzelfz0  13691  sqlecan  14258  hashf1lem2  14505  ccatsymb  14630  lo1le  15700  fsumss  15773  ntrivcvgfvn0  15947  fprodss  15996  smupvallem  16529  zeqzmulgcd  16556  lcmgcdlem  16653  lcmdvds  16655  lcmfunsnlem2lem1  16685  coprmproddvdslem  16709  cncongr2  16715  exprmfct  16751  infpnlem1  16957  prmdvdsprmop  17090  prmgaplem7  17104  prmlem0  17153  sscfn2  17879  isssc  17881  iszeroi  18076  funcsetcestrclem8  18231  dirge  18673  efgval  19759  dmdprd  20042  dprdw  20054  rhmsubclem4  20710  lpigen  21368  psrbaglefi  21969  matvscl  22458  scmatghm  22560  slesolinv  22707  cpmatacl  22743  pnfnei  23249  mnfnei  23250  cmpcld  23431  isfildlem  23886  metrest  24558  blval2  24596  iscmet3lem2  25345  ivthlem3  25507  mbfi1fseqlem4  25773  itg2seq  25797  aalioulem6  26397  taylthlem2  26434  chpchtsum  27281  dchrmulcl  27311  bcmono  27339  nosupno  27766  nosupbday  27768  noinfno  27781  noinfbday  27783  nocvxminlem  27840  cuteq1  27896  cgrg3col4  28879  brbtwn2  28938  axeuclid  28996  umgredg  29173  pthdivtx  29765  pthdlem1  29802  shsvs  31355  cnlnssadj  32112  atexch  32413  mdsymlem5  32439  disjxpin  32610  sigaclci  34096  fnrelpredd  35065  satfv0  35326  satffunlem2lem1  35372  dmopab3rexdif  35373  elfuns  35879  altopth1  35929  btwnexch2  35987  ifscgr  36008  colinbtwnle  36082  trer  36282  elicc3  36283  bj-imdirval3  37150  bj-finsumval0  37251  difunieq  37340  fvineqsneu  37377  fvineqsneq  37378  poimirlem27  37607  poimir  37613  cnambfre  37628  itg2addnclem2  37632  itg2addnc  37634  areacirclem1  37668  heiborlem4  37774  elghomlem2OLD  37846  rngo2  37867  ispridl2  37998  ispridlc  38030  iss2  38300  membpartlem19  38767  paddasslem14  39790  ispsubcl2N  39904  cdleme29ex  40331  cdlemefr29exN  40359  eldiophss  42730  rencldnfilem  42776  oaabsb  43256  cantnfresb  43286  tfsconcatrn  43304  naddwordnexlem1  43359  clsk1indlem3  44005  ntrneikb  44056  mnuop3d  44240  ax6e2ndeq  44530  suctrALT2  44808  2reu3  47025  iccpartiltu  47296  bgoldbtbndlem2  47680  grtrimap  47797  grimgrtri  47798  itschlc0xyqsol1  48500  elsetrecslem  48791  aacllem  48895