Theorem adantrd 493

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  im2anan9  621  jaoa  955  prlem1  1054  cad0  1620  cad0OLD  1621  dfsb1  2481  unineq  4278  dfopif  4871  elssabg  5337  exopxfr2  5845  tz7.7  6391  oneqmini  6417  fvun1  6983  fconst5  7207  fpropnf1  7266  isomin  7334  isofrlem  7337  poxp  8114  poseq  8144  tposfo2  8234  onfununi  8341  tfrlem9a  8386  oecl  8537  oawordri  8550  omwordri  8572  odi  8579  pssnn  9168  pssnnOLD  9265  prdom2  10001  acni2  10041  cardinfima  10092  cfslb2n  10263  infpssrlem4  10301  axdc3lem4  10448  brdom6disj  10527  tskr1om  10762  indpi  10902  1idpr  11024  1re  11214  mulge0  11732  infm3  12173  uzind  12654  suprfinzcl  12676  uzwo  12895  xrlttr  13119  xmullem2  13244  snunico  13456  fzen  13518  fz0fzelfz0  13607  sqlecan  14173  hashf1lem2  14417  ccatsymb  14532  lo1le  15598  fsumss  15671  ntrivcvgfvn0  15845  fprodss  15892  smupvallem  16424  zeqzmulgcd  16451  lcmgcdlem  16543  lcmdvds  16545  lcmfunsnlem2lem1  16575  coprmproddvdslem  16599  cncongr2  16605  exprmfct  16641  infpnlem1  16843  prmdvdsprmop  16976  prmgaplem7  16990  prmlem0  17039  sscfn2  17765  isssc  17767  iszeroi  17959  funcsetcestrclem8  18114  dirge  18556  efgval  19585  dmdprd  19868  dprdw  19880  lpigen  20894  psrbaglefi  21485  psrbaglefiOLD  21486  matvscl  21933  scmatghm  22035  slesolinv  22182  cpmatacl  22218  pnfnei  22724  mnfnei  22725  cmpcld  22906  isfildlem  23361  metrest  24033  blval2  24071  iscmet3lem2  24809  ivthlem3  24970  mbfi1fseqlem4  25236  itg2seq  25260  aalioulem6  25850  chpchtsum  26722  dchrmulcl  26752  bcmono  26780  nosupno  27206  nosupbday  27208  noinfno  27221  noinfbday  27223  nocvxminlem  27279  cuteq1  27334  cgrg3col4  28104  brbtwn2  28163  axeuclid  28221  umgredg  28398  pthdivtx  28986  pthdlem1  29023  shsvs  30576  cnlnssadj  31333  atexch  31634  mdsymlem5  31660  disjxpin  31819  sigaclci  33130  fnrelpredd  34092  satfv0  34349  satffunlem2lem1  34395  dmopab3rexdif  34396  elfuns  34887  altopth1  34937  btwnexch2  34995  ifscgr  35016  colinbtwnle  35090  trer  35201  elicc3  35202  bj-imdirval3  36065  bj-finsumval0  36166  difunieq  36255  fvineqsneu  36292  fvineqsneq  36293  poimirlem27  36515  poimir  36521  cnambfre  36536  itg2addnclem2  36540  itg2addnc  36542  areacirclem1  36576  heiborlem4  36682  elghomlem2OLD  36754  rngo2  36775  ispridl2  36906  ispridlc  36938  iss2  37213  membpartlem19  37681  paddasslem14  38704  ispsubcl2N  38818  cdleme29ex  39245  cdlemefr29exN  39273  eldiophss  41512  rencldnfilem  41558  oaabsb  42044  cantnfresb  42074  tfsconcatrn  42092  naddwordnexlem1  42148  clsk1indlem3  42794  ntrneikb  42845  mnuop3d  43030  ax6e2ndeq  43320  suctrALT2  43598  2reu3  45818  iccpartiltu  46090  bgoldbtbndlem2  46474  rhmsubclem4  46987  itschlc0xyqsol1  47452  elsetrecslem  47744  aacllem  47848