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  621  jaoa  958  prlem1  1055  cad0  1620  dfsb1  2486  unineq  4242  dfopif  4828  elssabg  5290  exopxfr2  5801  tz7.7  6351  oneqmini  6378  fvun1  6933  fconst5  7162  fpropnf1  7223  f1ounsn  7228  isomin  7293  isofrlem  7296  poxp  8080  poseq  8110  tposfo2  8201  onfununi  8283  tfrlem9a  8327  oecl  8474  oawordri  8487  omwordri  8509  odi  8516  pssnn  9105  prdom2  9928  acni2  9968  cardinfima  10019  cfslb2n  10190  infpssrlem4  10228  axdc3lem4  10375  brdom6disj  10454  tskr1om  10690  indpi  10830  1idpr  10952  1re  11144  mulge0  11667  infm3  12113  uzind  12596  suprfinzcl  12618  uzwo  12836  xrlttr  13066  xmullem2  13192  snunico  13407  fzen  13469  fz0fzelfz0  13562  sqlecan  14144  hashf1lem2  14391  ccatsymb  14518  lo1le  15587  fsumss  15660  ntrivcvgfvn0  15834  fprodss  15883  smupvallem  16422  zeqzmulgcd  16449  lcmgcdlem  16545  lcmdvds  16547  lcmfunsnlem2lem1  16577  coprmproddvdslem  16601  cncongr2  16607  exprmfct  16643  infpnlem1  16850  prmdvdsprmop  16983  prmgaplem7  16997  prmlem0  17045  sscfn2  17754  isssc  17756  iszeroi  17945  funcsetcestrclem8  18097  dirge  18538  efgval  19658  dmdprd  19941  dprdw  19953  rhmsubclem4  20633  lpigen  21302  psrbaglefi  21894  matvscl  22387  scmatghm  22489  slesolinv  22636  cpmatacl  22672  pnfnei  23176  mnfnei  23177  cmpcld  23358  isfildlem  23813  metrest  24480  blval2  24518  iscmet3lem2  25260  ivthlem3  25422  mbfi1fseqlem4  25687  itg2seq  25711  aalioulem6  26313  taylthlem2  26350  chpchtsum  27198  dchrmulcl  27228  bcmono  27256  nosupno  27683  nosupbday  27685  noinfno  27698  noinfbday  27700  nocvxminlem  27762  cuteq1  27825  oncutlt  28272  oniso  28279  bdayn0p1  28377  bdayfinbndlem2  28476  z12sge0  28491  cgrg3col4  28937  brbtwn2  28990  axeuclid  29048  umgredg  29223  pthdivtx  29812  pthdlem1  29851  shsvs  31411  cnlnssadj  32168  atexch  32469  mdsymlem5  32495  disjxpin  32675  fldextrspunlsplem  33851  sigaclci  34310  fnrelpredd  35268  satfv0  35574  satffunlem2lem1  35620  dmopab3rexdif  35621  elfuns  36129  altopth1  36181  btwnexch2  36239  ifscgr  36260  colinbtwnle  36334  trer  36532  elicc3  36533  bj-imdirval3  37439  bj-finsumval0  37540  difunieq  37629  fvineqsneu  37666  fvineqsneq  37667  poimirlem27  37898  poimir  37904  cnambfre  37919  itg2addnclem2  37923  itg2addnc  37925  areacirclem1  37959  heiborlem4  38065  elghomlem2OLD  38137  rngo2  38158  ispridl2  38289  ispridlc  38321  iss2  38595  membpartlem19  39165  paddasslem14  40209  ispsubcl2N  40323  cdleme29ex  40750  cdlemefr29exN  40778  eldiophss  43131  rencldnfilem  43177  oaabsb  43651  cantnfresb  43681  tfsconcatrn  43699  naddwordnexlem1  43754  clsk1indlem3  44399  ntrneikb  44450  mnuop3d  44627  ax6e2ndeq  44915  suctrALT2  45192  relpmin  45308  relpfrlem  45309  2reu3  47470  iccpartiltu  47782  bgoldbtbndlem2  48166  grtrimap  48308  grimgrtri  48309  isubgr3stgrlem6  48331  isubgr3stgr  48335  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem4  48479  itschlc0xyqsol1  49126  resipos  49334  elsetrecslem  50058  aacllem  50160