Theorem adantrd 492

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  im2anan9  626  jaoa  963  prlem1  1060  cad0  1625  dfsb1  2489  unineq  4216  dfopif  4801  elssabg  5271  exopxfr2  5786  tz7.7  6336  oneqmini  6363  fvun1  6918  fconst5  7150  fpropnf1  7211  f1ounsn  7216  isomin  7281  isofrlem  7284  poxp  8068  poseq  8098  tposfo2  8189  onfununi  8271  tfrlem9a  8315  oecl  8462  oawordri  8475  omwordri  8497  odi  8504  pssnn  9093  prdom2  9919  acni2  9959  cardinfima  10010  cfslb2n  10181  infpssrlem4  10219  axdc3lem4  10366  brdom6disj  10445  tskr1om  10681  indpi  10821  1idpr  10943  1re  11135  mulge0  11659  infm3  12106  uzind  12612  suprfinzcl  12634  uzwo  12852  xrlttr  13082  xmullem2  13208  snunico  13423  fzen  13486  fz0fzelfz0  13579  sqlecan  14162  hashf1lem2  14409  ccatsymb  14536  lo1le  15605  fsumss  15678  ntrivcvgfvn0  15855  fprodss  15904  smupvallem  16443  zeqzmulgcd  16470  lcmgcdlem  16566  lcmdvds  16568  lcmfunsnlem2lem1  16598  coprmproddvdslem  16622  cncongr2  16628  exprmfct  16665  infpnlem1  16872  prmdvdsprmop  17005  prmgaplem7  17019  prmlem0  17067  sscfn2  17776  isssc  17778  iszeroi  17967  funcsetcestrclem8  18119  dirge  18560  efgval  19683  dmdprd  19966  dprdw  19978  rhmsubclem4  20660  lpigen  21328  psrbaglefi  21901  matvscl  22414  scmatghm  22516  slesolinv  22663  cpmatacl  22699  pnfnei  23203  mnfnei  23204  cmpcld  23385  isfildlem  23840  metrest  24507  blval2  24545  iscmet3lem2  25277  ivthlem3  25438  mbfi1fseqlem4  25703  itg2seq  25727  aalioulem6  26321  taylthlem2  26357  chpchtsum  27200  dchrmulcl  27230  bcmono  27258  nosupno  27685  nosupbday  27687  noinfno  27700  noinfbday  27702  nocvxminlem  27764  cuteq1  27827  oncutlt  28274  oniso  28281  bdayn0p1  28379  bdayfinbndlem2  28478  z12sge0  28493  cgrg3col4  28939  brbtwn2  28992  axeuclid  29050  umgredg  29225  pthdivtx  29813  pthdlem1  29852  shsvs  31412  cnlnssadj  32169  atexch  32470  mdsymlem5  32496  disjxpin  32677  fldextrspunlsplem  33857  sigaclci  34316  fnrelpredd  35272  satfv0  35586  satffunlem2lem1  35632  dmopab3rexdif  35633  elfuns  36141  altopth1  36193  btwnexch2  36251  ifscgr  36272  colinbtwnle  36346  trer  36544  elicc3  36545  bj-imdirval3  37544  bj-finsumval0  37645  difunieq  37736  fvineqsneu  37773  fvineqsneq  37774  poimirlem27  38014  poimir  38020  cnambfre  38035  itg2addnclem2  38039  itg2addnc  38041  areacirclem1  38075  heiborlem4  38181  elghomlem2OLD  38253  rngo2  38274  ispridl2  38405  ispridlc  38437  iss2  38711  membpartlem19  39281  paddasslem14  40325  ispsubcl2N  40439  cdleme29ex  40866  cdlemefr29exN  40894  eldiophss  43223  rencldnfilem  43265  oaabsb  43739  cantnfresb  43769  tfsconcatrn  43787  naddwordnexlem1  43842  clsk1indlem3  44487  ntrneikb  44538  mnuop3d  44715  ax6e2ndeq  45003  suctrALT2  45280  relpmin  45396  relpfrlem  45397  2reu3  47573  iccpartiltu  47897  bgoldbtbndlem2  48297  grtrimap  48439  grimgrtri  48440  isubgr3stgrlem6  48462  isubgr3stgr  48466  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem4  48610  itschlc0xyqsol1  49257  resipos  49465  elsetrecslem  50189  aacllem  50291