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  1619  dfsb1  2483  unineq  4238  dfopif  4824  elssabg  5286  exopxfr2  5791  tz7.7  6341  oneqmini  6368  fvun1  6923  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  9091  prdom2  9914  acni2  9954  cardinfima  10005  cfslb2n  10176  infpssrlem4  10214  axdc3lem4  10361  brdom6disj  10440  tskr1om  10676  indpi  10816  1idpr  10938  1re  11130  mulge0  11653  infm3  12099  uzind  12582  suprfinzcl  12604  uzwo  12822  xrlttr  13052  xmullem2  13178  snunico  13393  fzen  13455  fz0fzelfz0  13548  sqlecan  14130  hashf1lem2  14377  ccatsymb  14504  lo1le  15573  fsumss  15646  ntrivcvgfvn0  15820  fprodss  15869  smupvallem  16408  zeqzmulgcd  16435  lcmgcdlem  16531  lcmdvds  16533  lcmfunsnlem2lem1  16563  coprmproddvdslem  16587  cncongr2  16593  exprmfct  16629  infpnlem1  16836  prmdvdsprmop  16969  prmgaplem7  16983  prmlem0  17031  sscfn2  17740  isssc  17742  iszeroi  17931  funcsetcestrclem8  18083  dirge  18524  efgval  19644  dmdprd  19927  dprdw  19939  rhmsubclem4  20619  lpigen  21288  psrbaglefi  21880  matvscl  22373  scmatghm  22475  slesolinv  22622  cpmatacl  22658  pnfnei  23162  mnfnei  23163  cmpcld  23344  isfildlem  23799  metrest  24466  blval2  24504  iscmet3lem2  25246  ivthlem3  25408  mbfi1fseqlem4  25673  itg2seq  25697  aalioulem6  26299  taylthlem2  26336  chpchtsum  27184  dchrmulcl  27214  bcmono  27242  nosupno  27669  nosupbday  27671  noinfno  27684  noinfbday  27686  nocvxminlem  27744  cuteq1  27805  onscutlt  28232  onsiso  28236  bdayn0p1  28327  zs12ge0  28432  cgrg3col4  28874  brbtwn2  28927  axeuclid  28985  umgredg  29160  pthdivtx  29749  pthdlem1  29788  shsvs  31347  cnlnssadj  32104  atexch  32405  mdsymlem5  32431  disjxpin  32612  fldextrspunlsplem  33779  sigaclci  34238  fnrelpredd  35196  satfv0  35501  satffunlem2lem1  35547  dmopab3rexdif  35548  elfuns  36056  altopth1  36108  btwnexch2  36166  ifscgr  36187  colinbtwnle  36261  trer  36459  elicc3  36460  bj-imdirval3  37328  bj-finsumval0  37429  difunieq  37518  fvineqsneu  37555  fvineqsneq  37556  poimirlem27  37787  poimir  37793  cnambfre  37808  itg2addnclem2  37812  itg2addnc  37814  areacirclem1  37848  heiborlem4  37954  elghomlem2OLD  38026  rngo2  38047  ispridl2  38178  ispridlc  38210  iss2  38476  membpartlem19  39009  paddasslem14  40032  ispsubcl2N  40146  cdleme29ex  40573  cdlemefr29exN  40601  eldiophss  42958  rencldnfilem  43004  oaabsb  43478  cantnfresb  43508  tfsconcatrn  43526  naddwordnexlem1  43581  clsk1indlem3  44226  ntrneikb  44277  mnuop3d  44454  ax6e2ndeq  44742  suctrALT2  45019  relpmin  45135  relpfrlem  45136  2reu3  47298  iccpartiltu  47610  bgoldbtbndlem2  47994  grtrimap  48136  grimgrtri  48137  isubgr3stgrlem6  48159  isubgr3stgr  48163  pgnbgreunbgrlem1  48301  pgnbgreunbgrlem4  48307  itschlc0xyqsol1  48954  resipos  49162  elsetrecslem  49886  aacllem  49988