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  2510  unineq  4234  dfopif  4830  elssabg  5307  exopxfr2  5824  tz7.7  6383  oneqmini  6411  fvun1  6969  fconst5  7205  fpropnf1  7264  f1ounsn  7273  isomin  7338  isofrlem  7341  poxp  8126  poseq  8156  tposfo2  8247  onfununi  8330  tfrlem9a  8375  oecl  8524  oawordri  8537  omwordri  8559  odi  8566  pssnn  9163  prdom2  10009  acni2  10049  cardinfima  10100  cfslb2n  10270  infpssrlem4  10308  axdc3lem4  10455  brdom6disj  10535  tskr1om  10776  indpi  10916  1idpr  11038  1re  11232  mulge0  11756  infm3  12198  uzind  12713  suprfinzcl  12735  uzwo  12960  xrlttr  13191  xmullem2  13317  snunico  13532  fzen  13595  fz0fzelfz0  13689  sqlecan  14273  hashf1lem2  14521  ccatsymb  14648  lo1le  15739  fsumss  15811  ntrivcvgfvn0  15988  fprodss  16035  smupvallem  16573  zeqzmulgcd  16600  lcmgcdlem  16696  lcmdvds  16698  lcmfunsnlem2lem1  16728  coprmproddvdslem  16752  cncongr2  16758  exprmfct  16795  infpnlem1  17002  prmdvdsprmop  17135  prmgaplem7  17149  prmlem0  17197  sscfn2  17907  isssc  17909  iszeroi  18098  funcsetcestrclem8  18250  dirge  18691  efgval  19844  dmdprd  20127  dprdw  20139  rhmsubclem4  20850  lpigen  21566  psrbaglefi  22141  matvscl  22653  scmatghm  22755  slesolinv  22905  cpmatacl  22941  pnfnei  23445  mnfnei  23446  cmpcld  23627  isfildlem  24083  metrest  24750  blval2  24788  iscmet3lem2  25520  ivthlem3  25681  mbfi1fseqlem4  25946  itg2seq  25970  aalioulem6  26573  taylthlem2  26610  chpchtsum  27455  dchrmulcl  27485  bcmono  27513  nosupno  27939  nosupbday  27941  noinfno  27954  noinfbday  27956  nocvxminlem  28019  cuteq1  28082  oncutlt  28529  oniso  28536  bdayn0p1  28634  bdayfinbndlem2  28733  z12sge0  28748  cgrg3col4  29251  brbtwn2  29362  axeuclid  29420  umgredg  29595  pthdivtx  30191  pthdlem1  30231  shsvs  31804  cnlnssadj  32561  atexch  32862  mdsymlem5  32888  disjxpin  33061  fldextrspunlsplem  34183  sigaclci  34642  fnrelpredd  35596  satfv0  35937  satffunlem2lem1  35983  dmopab3rexdif  35984  elfuns  36492  altopth1  36545  btwnexch2  36603  ifscgr  36624  colinbtwnle  36698  trer  36935  elicc3  36936  bj-imdirval3  37936  bj-finsumval0  38037  difunieq  38128  fvineqsneu  38165  fvineqsneq  38166  poimirlem27  38396  poimir  38402  cnambfre  38417  itg2addnclem2  38421  itg2addnc  38423  areacirclem1  38457  heiborlem4  38564  elghomlem2OLD  38636  rngo2  38657  ispridl2  38788  ispridlc  38820  iss2  39092  membpartlem19  39662  paddasslem14  40706  ispsubcl2N  40820  cdleme29ex  41247  cdlemefr29exN  41275  eldiophss  43619  rencldnfilem  43661  oaabsb  44135  cantnfresb  44165  tfsconcatrn  44183  naddwordnexlem1  44238  clsk1indlem3  44883  ntrneikb  44934  mnuop3d  45095  ax6e2ndeq  45382  suctrALT2  45659  relpmin  45775  relpfrlem  45776  2reu3  47998  iccpartiltu  48322  bgoldbtbndlem2  48722  grtrimap  48864  grimgrtri  48865  isubgr3stgrlem6  48887  isubgr3stgr  48891  pgnbgreunbgrlem1  49029  pgnbgreunbgrlem4  49035  itschlc0xyqsol1  49696  resipos  49901  elsetrecslem  50625  aacllem  50772