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  620  jaoa  957  prlem1  1054  cad0  1618  dfsb1  2479  unineq  4247  dfopif  4830  elssabg  5293  exopxfr2  5798  tz7.7  6346  oneqmini  6373  fvun1  6934  fconst5  7162  fpropnf1  7224  f1ounsn  7229  isomin  7294  isofrlem  7297  poxp  8084  poseq  8114  tposfo2  8205  onfununi  8287  tfrlem9a  8331  oecl  8478  oawordri  8491  omwordri  8513  odi  8520  pssnn  9109  prdom2  9935  acni2  9975  cardinfima  10026  cfslb2n  10197  infpssrlem4  10235  axdc3lem4  10382  brdom6disj  10461  tskr1om  10696  indpi  10836  1idpr  10958  1re  11150  mulge0  11672  infm3  12118  uzind  12602  suprfinzcl  12624  uzwo  12846  xrlttr  13076  xmullem2  13201  snunico  13416  fzen  13478  fz0fzelfz0  13571  sqlecan  14150  hashf1lem2  14397  ccatsymb  14523  lo1le  15594  fsumss  15667  ntrivcvgfvn0  15841  fprodss  15890  smupvallem  16429  zeqzmulgcd  16456  lcmgcdlem  16552  lcmdvds  16554  lcmfunsnlem2lem1  16584  coprmproddvdslem  16608  cncongr2  16614  exprmfct  16650  infpnlem1  16857  prmdvdsprmop  16990  prmgaplem7  17004  prmlem0  17052  sscfn2  17756  isssc  17758  iszeroi  17947  funcsetcestrclem8  18099  dirge  18538  efgval  19623  dmdprd  19906  dprdw  19918  rhmsubclem4  20573  lpigen  21221  psrbaglefi  21811  matvscl  22294  scmatghm  22396  slesolinv  22543  cpmatacl  22579  pnfnei  23083  mnfnei  23084  cmpcld  23265  isfildlem  23720  metrest  24388  blval2  24426  iscmet3lem2  25168  ivthlem3  25330  mbfi1fseqlem4  25595  itg2seq  25619  aalioulem6  26221  taylthlem2  26258  chpchtsum  27106  dchrmulcl  27136  bcmono  27164  nosupno  27591  nosupbday  27593  noinfno  27606  noinfbday  27608  nocvxminlem  27665  cuteq1  27722  onscutlt  28141  onsiso  28145  bdayn0p1  28234  zs12ge0  28318  cgrg3col4  28756  brbtwn2  28808  axeuclid  28866  umgredg  29041  pthdivtx  29630  pthdlem1  29669  shsvs  31225  cnlnssadj  31982  atexch  32283  mdsymlem5  32309  disjxpin  32490  fldextrspunlsplem  33641  sigaclci  34095  fnrelpredd  35052  satfv0  35318  satffunlem2lem1  35364  dmopab3rexdif  35365  elfuns  35876  altopth1  35926  btwnexch2  35984  ifscgr  36005  colinbtwnle  36079  trer  36277  elicc3  36278  bj-imdirval3  37145  bj-finsumval0  37246  difunieq  37335  fvineqsneu  37372  fvineqsneq  37373  poimirlem27  37614  poimir  37620  cnambfre  37635  itg2addnclem2  37639  itg2addnc  37641  areacirclem1  37675  heiborlem4  37781  elghomlem2OLD  37853  rngo2  37874  ispridl2  38005  ispridlc  38037  iss2  38299  membpartlem19  38776  paddasslem14  39800  ispsubcl2N  39914  cdleme29ex  40341  cdlemefr29exN  40369  eldiophss  42735  rencldnfilem  42781  oaabsb  43256  cantnfresb  43286  tfsconcatrn  43304  naddwordnexlem1  43359  clsk1indlem3  44005  ntrneikb  44056  mnuop3d  44233  ax6e2ndeq  44522  suctrALT2  44799  relpmin  44915  relpfrlem  44916  2reu3  47084  iccpartiltu  47396  bgoldbtbndlem2  47780  grtrimap  47920  grimgrtri  47921  isubgr3stgrlem6  47943  isubgr3stgr  47947  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem4  48082  itschlc0xyqsol1  48728  resipos  48936  elsetrecslem  49661  aacllem  49763