Theorem adantrd 490

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  im2anan9  618  jaoa  952  prlem1  1051  cad0  1617  cad0OLD  1618  dfsb1  2478  unineq  4276  dfopif  4869  elssabg  5335  exopxfr2  5843  tz7.7  6389  oneqmini  6415  fvun1  6981  fconst5  7208  fpropnf1  7268  isomin  7336  isofrlem  7339  poxp  8116  poseq  8146  tposfo2  8236  onfununi  8343  tfrlem9a  8388  oecl  8539  oawordri  8552  omwordri  8574  odi  8581  pssnn  9170  pssnnOLD  9267  prdom2  10003  acni2  10043  cardinfima  10094  cfslb2n  10265  infpssrlem4  10303  axdc3lem4  10450  brdom6disj  10529  tskr1om  10764  indpi  10904  1idpr  11026  1re  11218  mulge0  11736  infm3  12177  uzind  12658  suprfinzcl  12680  uzwo  12899  xrlttr  13123  xmullem2  13248  snunico  13460  fzen  13522  fz0fzelfz0  13611  sqlecan  14177  hashf1lem2  14421  ccatsymb  14536  lo1le  15602  fsumss  15675  ntrivcvgfvn0  15849  fprodss  15896  smupvallem  16428  zeqzmulgcd  16455  lcmgcdlem  16547  lcmdvds  16549  lcmfunsnlem2lem1  16579  coprmproddvdslem  16603  cncongr2  16609  exprmfct  16645  infpnlem1  16847  prmdvdsprmop  16980  prmgaplem7  16994  prmlem0  17043  sscfn2  17769  isssc  17771  iszeroi  17963  funcsetcestrclem8  18118  dirge  18560  efgval  19626  dmdprd  19909  dprdw  19921  lpigen  21094  psrbaglefi  21704  psrbaglefiOLD  21705  matvscl  22153  scmatghm  22255  slesolinv  22402  cpmatacl  22438  pnfnei  22944  mnfnei  22945  cmpcld  23126  isfildlem  23581  metrest  24253  blval2  24291  iscmet3lem2  25040  ivthlem3  25202  mbfi1fseqlem4  25468  itg2seq  25492  aalioulem6  26086  chpchtsum  26958  dchrmulcl  26988  bcmono  27016  nosupno  27442  nosupbday  27444  noinfno  27457  noinfbday  27459  nocvxminlem  27515  cuteq1  27571  cgrg3col4  28371  brbtwn2  28430  axeuclid  28488  umgredg  28665  pthdivtx  29253  pthdlem1  29290  shsvs  30843  cnlnssadj  31600  atexch  31901  mdsymlem5  31927  disjxpin  32086  sigaclci  33428  fnrelpredd  34390  satfv0  34647  satffunlem2lem1  34693  dmopab3rexdif  34694  elfuns  35191  altopth1  35241  btwnexch2  35299  ifscgr  35320  colinbtwnle  35394  trer  35504  elicc3  35505  bj-imdirval3  36368  bj-finsumval0  36469  difunieq  36558  fvineqsneu  36595  fvineqsneq  36596  poimirlem27  36818  poimir  36824  cnambfre  36839  itg2addnclem2  36843  itg2addnc  36845  areacirclem1  36879  heiborlem4  36985  elghomlem2OLD  37057  rngo2  37078  ispridl2  37209  ispridlc  37241  iss2  37516  membpartlem19  37984  paddasslem14  39007  ispsubcl2N  39121  cdleme29ex  39548  cdlemefr29exN  39576  eldiophss  41814  rencldnfilem  41860  oaabsb  42346  cantnfresb  42376  tfsconcatrn  42394  naddwordnexlem1  42450  clsk1indlem3  43096  ntrneikb  43147  mnuop3d  43332  ax6e2ndeq  43622  suctrALT2  43900  2reu3  46116  iccpartiltu  46388  bgoldbtbndlem2  46772  rhmsubclem4  47075  itschlc0xyqsol1  47539  elsetrecslem  47831  aacllem  47935