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  2486  unineq  4268  dfopif  4851  elssabg  5318  exopxfr2  5829  tz7.7  6383  oneqmini  6410  fvun1  6975  fconst5  7203  fpropnf1  7265  f1ounsn  7270  isomin  7335  isofrlem  7338  poxp  8132  poseq  8162  tposfo2  8253  onfununi  8360  tfrlem9a  8405  oecl  8554  oawordri  8567  omwordri  8589  odi  8596  pssnn  9187  prdom2  10025  acni2  10065  cardinfima  10116  cfslb2n  10287  infpssrlem4  10325  axdc3lem4  10472  brdom6disj  10551  tskr1om  10786  indpi  10926  1idpr  11048  1re  11240  mulge0  11760  infm3  12206  uzind  12690  suprfinzcl  12712  uzwo  12932  xrlttr  13161  xmullem2  13286  snunico  13501  fzen  13563  fz0fzelfz0  13656  sqlecan  14232  hashf1lem2  14479  ccatsymb  14605  lo1le  15673  fsumss  15746  ntrivcvgfvn0  15920  fprodss  15969  smupvallem  16507  zeqzmulgcd  16534  lcmgcdlem  16630  lcmdvds  16632  lcmfunsnlem2lem1  16662  coprmproddvdslem  16686  cncongr2  16692  exprmfct  16728  infpnlem1  16935  prmdvdsprmop  17068  prmgaplem7  17082  prmlem0  17130  sscfn2  17836  isssc  17838  iszeroi  18027  funcsetcestrclem8  18179  dirge  18618  efgval  19703  dmdprd  19986  dprdw  19998  rhmsubclem4  20653  lpigen  21301  psrbaglefi  21891  matvscl  22374  scmatghm  22476  slesolinv  22623  cpmatacl  22659  pnfnei  23163  mnfnei  23164  cmpcld  23345  isfildlem  23800  metrest  24468  blval2  24506  iscmet3lem2  25249  ivthlem3  25411  mbfi1fseqlem4  25676  itg2seq  25700  aalioulem6  26302  taylthlem2  26339  chpchtsum  27187  dchrmulcl  27217  bcmono  27245  nosupno  27672  nosupbday  27674  noinfno  27687  noinfbday  27689  nocvxminlem  27746  cuteq1  27803  onscutlt  28222  onsiso  28226  bdayn0p1  28315  zs12ge0  28399  cgrg3col4  28837  brbtwn2  28889  axeuclid  28947  umgredg  29122  pthdivtx  29714  pthdlem1  29753  shsvs  31309  cnlnssadj  32066  atexch  32367  mdsymlem5  32393  disjxpin  32574  fldextrspunlsplem  33719  sigaclci  34168  fnrelpredd  35125  satfv0  35385  satffunlem2lem1  35431  dmopab3rexdif  35432  elfuns  35938  altopth1  35988  btwnexch2  36046  ifscgr  36067  colinbtwnle  36141  trer  36339  elicc3  36340  bj-imdirval3  37207  bj-finsumval0  37308  difunieq  37397  fvineqsneu  37434  fvineqsneq  37435  poimirlem27  37676  poimir  37682  cnambfre  37697  itg2addnclem2  37701  itg2addnc  37703  areacirclem1  37737  heiborlem4  37843  elghomlem2OLD  37915  rngo2  37936  ispridl2  38067  ispridlc  38099  iss2  38367  membpartlem19  38834  paddasslem14  39857  ispsubcl2N  39971  cdleme29ex  40398  cdlemefr29exN  40426  eldiophss  42772  rencldnfilem  42818  oaabsb  43293  cantnfresb  43323  tfsconcatrn  43341  naddwordnexlem1  43396  clsk1indlem3  44042  ntrneikb  44093  mnuop3d  44270  ax6e2ndeq  44559  suctrALT2  44836  relpmin  44952  relpfrlem  44953  2reu3  47119  iccpartiltu  47416  bgoldbtbndlem2  47800  grtrimap  47940  grimgrtri  47941  isubgr3stgrlem6  47963  isubgr3stgr  47967  itschlc0xyqsol1  48726  resipos  48929  elsetrecslem  49543  aacllem  49645