Theorem adantrd 497

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  im2anan9  632  jaoa  970  prlem1  1070  cad0  1651  dfsb1  2513  unineq  4236  dfopif  4842  elssabg  5311  exopxfr2  5832  tz7.7  6414  oneqmini  6442  fvun1  7007  fconst5  7243  fpropnf1  7302  f1ounsn  7311  isomin  7376  isofrlem  7379  poxp  8177  poseq  8212  tposfo2  8304  onfununi  8387  tfrlem9a  8432  oecl  8583  oawordri  8596  omwordri  8618  odi  8625  pssnn  9222  prdom2  10124  acni2  10164  cardinfima  10215  cfslb2n  10385  infpssrlem4  10423  axdc3lem4  10570  brdom6disj  10650  tskr1om  10891  indpi  11031  1idpr  11153  1re  11347  mulge0  11874  infm3  12316  uzind  12831  suprfinzcl  12853  uzwo  13078  xrlttr  13309  xmullem2  13435  snunico  13650  fzen  13714  fz0fzelfz0  13808  sqlecan  14393  hashf1lem2  14642  ccatsymb  14769  lo1le  15863  fsumss  15935  ntrivcvgfvn0  16112  fprodss  16159  smupvallem  16697  zeqzmulgcd  16726  lcmgcdlem  16825  lcmdvds  16827  lcmfunsnlem2lem1  16857  coprmproddvdslem  16881  cncongr2  16887  exprmfct  16924  infpnlem1  17132  prmdvdsprmop  17265  prmgaplem7  17279  prmlem0  17327  sscfn2  18043  isssc  18045  iszeroi  18234  funcsetcestrclem8  18386  dirge  18827  efgval  19982  dmdprd  20265  dprdw  20277  rhmsubclem4  20991  lpigen  21710  psrbaglefi  22289  matvscl  22801  scmatghm  22903  slesolinv  23053  cpmatacl  23089  pnfnei  23593  mnfnei  23594  cmpcld  23775  isfildlem  24231  metrest  24898  blval2  24936  iscmet3lem2  25668  ivthlem3  25829  mbfi1fseqlem4  26094  itg2seq  26118  aalioulem6  26721  taylthlem2  26758  chpchtsum  27603  dchrmulcl  27633  bcmono  27661  nosupno  28117  nosupbday  28119  noinfno  28132  noinfbday  28134  nocvxminlem  28197  cuteq1  28260  oncutlt  28707  oniso  28714  bdayn0p1  28812  bdayfinbndlem2  28911  z12sge0  28926  cgrg3col4  29429  brbtwn2  29540  axeuclid  29598  umgredg  29773  pthdivtx  30369  pthdlem1  30409  shsvs  31982  cnlnssadj  32739  atexch  33040  mdsymlem5  33066  disjxpin  33280  fldextrspunlsplem  34416  sigaclci  34875  fnrelpredd  35845  weexenwe  35889  ptpconn  36206  satfv0  36331  satffunlem2lem1  36377  dmopab3rexdif  36378  elfuns  36892  altopth1  36945  btwnexch2  37003  ifscgr  37024  colinbtwnle  37098  trer  37319  elicc3  37320  mh-inf3f1  37544  bj-imdirval3  38373  bj-finsumval0  38474  difunieq  38565  fvineqsneu  38602  fvineqsneq  38603  poimirlem27  38833  poimir  38839  cnambfre  38854  itg2addnclem2  38858  itg2addnc  38860  areacirclem1  38894  heiborlem4  39014  elghomlem2OLD  39086  rngo2  39107  ispridl2  39238  ispridlc  39270  iss2  39542  membpartlem19  40112  paddasslem14  41156  ispsubcl2N  41270  cdleme29ex  41697  cdlemefr29exN  41725  eldiophss  44051  rencldnfilem  44093  oaabsb  44557  cantnfresb  44587  tfsconcatrn  44605  naddwordnexlem1  44660  clsk1indlem3  45304  ntrneikb  45355  mnuop3d  45516  ax6e2ndeq  45802  suctrALT2  46079  cocanss2  46183  relpmin  46206  relpfrlem  46207  2reu3  48454  iccpartiltu  48777  bgoldbtbndlem2  49177  grtrimap  49319  grimgrtri  49320  isubgr3stgrlem6  49342  isubgr3stgr  49346  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem4  49490  itschlc0xyqsol1  50209  resipos  50420  elsetrecslem  51198  aacllem  51367