Theorem adantrd 487

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  syldan  585  jaoa  941  prlem1  1038  cad0  1675  2eu3OLD  2684  unineq  4104  dfopif  4633  axsep  5016  elssabg  5053  exopxfr2  5512  tz7.7  6002  oneqmini  6027  fvun1  6529  fconst5  6743  fpropnf1  6796  isomin  6859  isofrlem  6862  poxp  7570  tposfo2  7657  onfununi  7721  tfrlem9a  7765  oecl  7901  oawordri  7914  omwordri  7936  odi  7943  pssnn  8466  prdom2  9162  acni2  9202  cardinfima  9253  cfslb2n  9425  infpssrlem4  9463  axdc3lem4  9610  brdom6disj  9689  tskr1om  9924  indpi  10064  1idpr  10186  1re  10376  mulge0  10893  infm3  11336  uzind  11821  suprfinzcl  11844  uzwo  12058  xrlttr  12283  xmullem2  12407  ioounsnOLD  12614  snunico  12616  fzen  12675  fz0fzelfz0  12764  sqlecan  13290  hashf1lem2  13554  lo1le  14790  fsumss  14863  ntrivcvgfvn0  15034  fprodss  15081  smupvallem  15611  zeqzmulgcd  15638  lcmgcdlem  15725  lcmdvds  15727  lcmfunsnlem2lem1  15757  coprmproddvdslem  15781  cncongr2  15787  exprmfct  15820  infpnlem1  16018  prmdvdsprmop  16151  prmgaplem7  16165  prmlem0  16211  sscfn2  16863  isssc  16865  iszeroi  17044  funcsetcestrclem8  17188  dirge  17623  efgval  18514  dmdprd  18784  dprdw  18796  ringadd2  18962  lpigen  19653  psrbaglefi  19769  matvscl  20641  scmatghm  20744  slesolinv  20892  cpmatacl  20928  pnfnei  21432  mnfnei  21433  cmpcld  21614  isfildlem  22069  metrest  22737  blval2  22775  iscmet3lem2  23498  ivthlem3  23657  mbfi1fseqlem4  23922  itg2seq  23946  aalioulem6  24529  chpchtsum  25396  dchrmulcl  25426  bcmono  25454  cgrg3col4  26202  brbtwn2  26254  axeuclid  26312  umgredg  26487  pthdivtx  27081  pthdlem1  27118  wwlksext2clwwlk  27454  shsvs  28754  cnlnssadj  29511  atexch  29812  mdsymlem5  29838  disjxpin  29964  sigaclci  30793  poseq  32342  nosupno  32438  nosupbday  32440  nocvxminlem  32482  elfuns  32611  altopth1  32661  btwnexch2  32719  ifscgr  32740  colinbtwnle  32814  trer  32899  elicc3  32900  bj-axsep  33370  bj-finsumval0  33749  poimirlem27  34062  poimir  34068  cnambfre  34083  itg2addnclem2  34087  itg2addnc  34089  areacirclem1  34125  heiborlem4  34237  elghomlem2OLD  34309  rngo2  34330  ispridl2  34461  ispridlc  34493  iss2  34740  paddasslem14  35987  ispsubcl2N  36101  cdleme29ex  36528  cdlemefr29exN  36556  eldiophss  38298  rencldnfilem  38344  clsk1indlem3  39297  ntrneikb  39348  ax6e2ndeq  39719  suctrALT2  40006  2reu3  42149  iccpartiltu  42390  bgoldbtbndlem2  42719  rhmsubclem4  43104  itschlc0xyqsol1  43502  elsetrecslem  43550  aacllem  43653