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  2515  unineq  4241  dfopif  4837  elssabg  5315  exopxfr2  5832  tz7.7  6390  oneqmini  6418  fvun1  6976  fconst5  7211  fpropnf1  7270  f1ounsn  7279  isomin  7344  isofrlem  7347  poxp  8130  poseq  8160  tposfo2  8251  onfununi  8334  tfrlem9a  8379  oecl  8528  oawordri  8541  omwordri  8563  odi  8570  pssnn  9160  prdom2  10006  acni2  10046  cardinfima  10097  cfslb2n  10267  infpssrlem4  10305  axdc3lem4  10452  brdom6disj  10531  tskr1om  10767  indpi  10907  1idpr  11029  1re  11223  mulge0  11747  infm3  12189  uzind  12704  suprfinzcl  12726  uzwo  12951  xrlttr  13181  xmullem2  13307  snunico  13522  fzen  13585  fz0fzelfz0  13679  sqlecan  14263  hashf1lem2  14511  ccatsymb  14638  lo1le  15727  fsumss  15799  ntrivcvgfvn0  15976  fprodss  16025  smupvallem  16563  zeqzmulgcd  16590  lcmgcdlem  16686  lcmdvds  16688  lcmfunsnlem2lem1  16718  coprmproddvdslem  16742  cncongr2  16748  exprmfct  16785  infpnlem1  16992  prmdvdsprmop  17125  prmgaplem7  17139  prmlem0  17187  sscfn2  17897  isssc  17899  iszeroi  18088  funcsetcestrclem8  18240  dirge  18681  efgval  19831  dmdprd  20114  dprdw  20126  rhmsubclem4  20837  lpigen  21553  psrbaglefi  22126  matvscl  22638  scmatghm  22740  slesolinv  22887  cpmatacl  22923  pnfnei  23427  mnfnei  23428  cmpcld  23609  isfildlem  24065  metrest  24732  blval2  24770  iscmet3lem2  25502  ivthlem3  25663  mbfi1fseqlem4  25928  itg2seq  25952  aalioulem6  26551  taylthlem2  26588  chpchtsum  27434  dchrmulcl  27464  bcmono  27492  nosupno  27918  nosupbday  27920  noinfno  27933  noinfbday  27935  nocvxminlem  27998  cuteq1  28061  oncutlt  28508  oniso  28515  bdayn0p1  28613  bdayfinbndlem2  28712  z12sge0  28727  cgrg3col4  29225  brbtwn2  29310  axeuclid  29368  umgredg  29543  pthdivtx  30139  pthdlem1  30179  shsvs  31746  cnlnssadj  32503  atexch  32804  mdsymlem5  32830  disjxpin  33004  fldextrspunlsplem  34127  sigaclci  34586  fnrelpredd  35540  satfv0  35887  satffunlem2lem1  35933  dmopab3rexdif  35934  elfuns  36442  altopth1  36494  btwnexch2  36552  ifscgr  36573  colinbtwnle  36647  trer  36884  elicc3  36885  bj-imdirval3  37885  bj-finsumval0  37986  difunieq  38077  fvineqsneu  38114  fvineqsneq  38115  poimirlem27  38355  poimir  38361  cnambfre  38376  itg2addnclem2  38380  itg2addnc  38382  areacirclem1  38416  heiborlem4  38523  elghomlem2OLD  38595  rngo2  38616  ispridl2  38747  ispridlc  38779  iss2  39051  membpartlem19  39621  paddasslem14  40665  ispsubcl2N  40779  cdleme29ex  41206  cdlemefr29exN  41234  eldiophss  43563  rencldnfilem  43605  oaabsb  44079  cantnfresb  44109  tfsconcatrn  44127  naddwordnexlem1  44182  clsk1indlem3  44827  ntrneikb  44878  mnuop3d  45039  ax6e2ndeq  45326  suctrALT2  45603  relpmin  45719  relpfrlem  45720  2reu3  47905  iccpartiltu  48229  bgoldbtbndlem2  48629  grtrimap  48771  grimgrtri  48772  isubgr3stgrlem6  48794  isubgr3stgr  48798  pgnbgreunbgrlem1  48936  pgnbgreunbgrlem4  48942  itschlc0xyqsol1  49603  resipos  49810  elsetrecslem  50534  aacllem  50678