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  1615  dfsb1  2484  unineq  4294  dfopif  4875  elssabg  5349  exopxfr2  5858  tz7.7  6412  oneqmini  6438  fvun1  7000  fconst5  7226  fpropnf1  7287  f1ounsn  7292  isomin  7357  isofrlem  7360  poxp  8152  poseq  8182  tposfo2  8273  onfununi  8380  tfrlem9a  8425  oecl  8574  oawordri  8587  omwordri  8609  odi  8616  pssnn  9207  prdom2  10044  acni2  10084  cardinfima  10135  cfslb2n  10306  infpssrlem4  10344  axdc3lem4  10491  brdom6disj  10570  tskr1om  10805  indpi  10945  1idpr  11067  1re  11259  mulge0  11779  infm3  12225  uzind  12708  suprfinzcl  12730  uzwo  12951  xrlttr  13179  xmullem2  13304  snunico  13516  fzen  13578  fz0fzelfz0  13671  sqlecan  14245  hashf1lem2  14492  ccatsymb  14617  lo1le  15685  fsumss  15758  ntrivcvgfvn0  15932  fprodss  15981  smupvallem  16517  zeqzmulgcd  16544  lcmgcdlem  16640  lcmdvds  16642  lcmfunsnlem2lem1  16672  coprmproddvdslem  16696  cncongr2  16702  exprmfct  16738  infpnlem1  16944  prmdvdsprmop  17077  prmgaplem7  17091  prmlem0  17140  sscfn2  17866  isssc  17868  iszeroi  18063  funcsetcestrclem8  18218  dirge  18661  efgval  19750  dmdprd  20033  dprdw  20045  rhmsubclem4  20705  lpigen  21363  psrbaglefi  21964  matvscl  22453  scmatghm  22555  slesolinv  22702  cpmatacl  22738  pnfnei  23244  mnfnei  23245  cmpcld  23426  isfildlem  23881  metrest  24553  blval2  24591  iscmet3lem2  25340  ivthlem3  25502  mbfi1fseqlem4  25768  itg2seq  25792  aalioulem6  26394  taylthlem2  26431  chpchtsum  27278  dchrmulcl  27308  bcmono  27336  nosupno  27763  nosupbday  27765  noinfno  27778  noinfbday  27780  nocvxminlem  27837  cuteq1  27893  cgrg3col4  28876  brbtwn2  28935  axeuclid  28993  umgredg  29170  pthdivtx  29762  pthdlem1  29799  shsvs  31352  cnlnssadj  32109  atexch  32410  mdsymlem5  32436  disjxpin  32608  sigaclci  34113  fnrelpredd  35082  satfv0  35343  satffunlem2lem1  35389  dmopab3rexdif  35390  elfuns  35897  altopth1  35947  btwnexch2  36005  ifscgr  36026  colinbtwnle  36100  trer  36299  elicc3  36300  bj-imdirval3  37167  bj-finsumval0  37268  difunieq  37357  fvineqsneu  37394  fvineqsneq  37395  poimirlem27  37634  poimir  37640  cnambfre  37655  itg2addnclem2  37659  itg2addnc  37661  areacirclem1  37695  heiborlem4  37801  elghomlem2OLD  37873  rngo2  37894  ispridl2  38025  ispridlc  38057  iss2  38326  membpartlem19  38793  paddasslem14  39816  ispsubcl2N  39930  cdleme29ex  40357  cdlemefr29exN  40385  eldiophss  42762  rencldnfilem  42808  oaabsb  43284  cantnfresb  43314  tfsconcatrn  43332  naddwordnexlem1  43387  clsk1indlem3  44033  ntrneikb  44084  mnuop3d  44267  ax6e2ndeq  44557  suctrALT2  44835  2reu3  47060  iccpartiltu  47347  bgoldbtbndlem2  47731  grtrimap  47851  grimgrtri  47852  isubgr3stgrlem6  47874  isubgr3stgr  47878  itschlc0xyqsol1  48616  elsetrecslem  48930  aacllem  49032