Theorem adantrd 490

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  im2anan9  618  jaoa  953  prlem1  1052  cad0  1611  cad0OLD  1612  dfsb1  2475  unineq  4280  dfopif  4875  elssabg  5342  exopxfr2  5851  tz7.7  6400  oneqmini  6426  fvun1  6994  fconst5  7224  fpropnf1  7283  isomin  7351  isofrlem  7354  poxp  8139  poseq  8169  tposfo2  8261  onfununi  8368  tfrlem9a  8413  oecl  8564  oawordri  8577  omwordri  8599  odi  8606  pssnn  9199  pssnnOLD  9296  prdom2  10037  acni2  10077  cardinfima  10128  cfslb2n  10299  infpssrlem4  10337  axdc3lem4  10484  brdom6disj  10563  tskr1om  10798  indpi  10938  1idpr  11060  1re  11252  mulge0  11770  infm3  12211  uzind  12692  suprfinzcl  12714  uzwo  12933  xrlttr  13159  xmullem2  13284  snunico  13496  fzen  13558  fz0fzelfz0  13647  sqlecan  14212  hashf1lem2  14457  ccatsymb  14572  lo1le  15638  fsumss  15711  ntrivcvgfvn0  15885  fprodss  15932  smupvallem  16465  zeqzmulgcd  16492  lcmgcdlem  16584  lcmdvds  16586  lcmfunsnlem2lem1  16616  coprmproddvdslem  16640  cncongr2  16646  exprmfct  16682  infpnlem1  16886  prmdvdsprmop  17019  prmgaplem7  17033  prmlem0  17082  sscfn2  17808  isssc  17810  iszeroi  18005  funcsetcestrclem8  18160  dirge  18602  efgval  19679  dmdprd  19962  dprdw  19974  rhmsubclem4  20628  lpigen  21232  psrbaglefi  21872  psrbaglefiOLD  21873  matvscl  22353  scmatghm  22455  slesolinv  22602  cpmatacl  22638  pnfnei  23144  mnfnei  23145  cmpcld  23326  isfildlem  23781  metrest  24453  blval2  24491  iscmet3lem2  25240  ivthlem3  25402  mbfi1fseqlem4  25668  itg2seq  25692  aalioulem6  26292  taylthlem2  26329  chpchtsum  27172  dchrmulcl  27202  bcmono  27230  nosupno  27656  nosupbday  27658  noinfno  27671  noinfbday  27673  nocvxminlem  27730  cuteq1  27786  cgrg3col4  28677  brbtwn2  28736  axeuclid  28794  umgredg  28971  pthdivtx  29563  pthdlem1  29600  shsvs  31153  cnlnssadj  31910  atexch  32211  mdsymlem5  32237  disjxpin  32399  sigaclci  33784  fnrelpredd  34745  satfv0  35001  satffunlem2lem1  35047  dmopab3rexdif  35048  elfuns  35544  altopth1  35594  btwnexch2  35652  ifscgr  35673  colinbtwnle  35747  trer  35833  elicc3  35834  bj-imdirval3  36696  bj-finsumval0  36797  difunieq  36886  fvineqsneu  36923  fvineqsneq  36924  poimirlem27  37153  poimir  37159  cnambfre  37174  itg2addnclem2  37178  itg2addnc  37180  areacirclem1  37214  heiborlem4  37320  elghomlem2OLD  37392  rngo2  37413  ispridl2  37544  ispridlc  37576  iss2  37848  membpartlem19  38315  paddasslem14  39338  ispsubcl2N  39452  cdleme29ex  39879  cdlemefr29exN  39907  eldiophss  42225  rencldnfilem  42271  oaabsb  42754  cantnfresb  42784  tfsconcatrn  42802  naddwordnexlem1  42858  clsk1indlem3  43504  ntrneikb  43555  mnuop3d  43739  ax6e2ndeq  44029  suctrALT2  44307  2reu3  46519  iccpartiltu  46791  bgoldbtbndlem2  47175  itschlc0xyqsol1  47917  elsetrecslem  48208  aacllem  48312