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  2480  unineq  4254  dfopif  4837  elssabg  5301  exopxfr2  5811  tz7.7  6361  oneqmini  6388  fvun1  6955  fconst5  7183  fpropnf1  7245  f1ounsn  7250  isomin  7315  isofrlem  7318  poxp  8110  poseq  8140  tposfo2  8231  onfununi  8313  tfrlem9a  8357  oecl  8504  oawordri  8517  omwordri  8539  odi  8546  pssnn  9138  prdom2  9966  acni2  10006  cardinfima  10057  cfslb2n  10228  infpssrlem4  10266  axdc3lem4  10413  brdom6disj  10492  tskr1om  10727  indpi  10867  1idpr  10989  1re  11181  mulge0  11703  infm3  12149  uzind  12633  suprfinzcl  12655  uzwo  12877  xrlttr  13107  xmullem2  13232  snunico  13447  fzen  13509  fz0fzelfz0  13602  sqlecan  14181  hashf1lem2  14428  ccatsymb  14554  lo1le  15625  fsumss  15698  ntrivcvgfvn0  15872  fprodss  15921  smupvallem  16460  zeqzmulgcd  16487  lcmgcdlem  16583  lcmdvds  16585  lcmfunsnlem2lem1  16615  coprmproddvdslem  16639  cncongr2  16645  exprmfct  16681  infpnlem1  16888  prmdvdsprmop  17021  prmgaplem7  17035  prmlem0  17083  sscfn2  17787  isssc  17789  iszeroi  17978  funcsetcestrclem8  18130  dirge  18569  efgval  19654  dmdprd  19937  dprdw  19949  rhmsubclem4  20604  lpigen  21252  psrbaglefi  21842  matvscl  22325  scmatghm  22427  slesolinv  22574  cpmatacl  22610  pnfnei  23114  mnfnei  23115  cmpcld  23296  isfildlem  23751  metrest  24419  blval2  24457  iscmet3lem2  25199  ivthlem3  25361  mbfi1fseqlem4  25626  itg2seq  25650  aalioulem6  26252  taylthlem2  26289  chpchtsum  27137  dchrmulcl  27167  bcmono  27195  nosupno  27622  nosupbday  27624  noinfno  27637  noinfbday  27639  nocvxminlem  27696  cuteq1  27753  onscutlt  28172  onsiso  28176  bdayn0p1  28265  zs12ge0  28349  cgrg3col4  28787  brbtwn2  28839  axeuclid  28897  umgredg  29072  pthdivtx  29664  pthdlem1  29703  shsvs  31259  cnlnssadj  32016  atexch  32317  mdsymlem5  32343  disjxpin  32524  fldextrspunlsplem  33675  sigaclci  34129  fnrelpredd  35086  satfv0  35352  satffunlem2lem1  35398  dmopab3rexdif  35399  elfuns  35910  altopth1  35960  btwnexch2  36018  ifscgr  36039  colinbtwnle  36113  trer  36311  elicc3  36312  bj-imdirval3  37179  bj-finsumval0  37280  difunieq  37369  fvineqsneu  37406  fvineqsneq  37407  poimirlem27  37648  poimir  37654  cnambfre  37669  itg2addnclem2  37673  itg2addnc  37675  areacirclem1  37709  heiborlem4  37815  elghomlem2OLD  37887  rngo2  37908  ispridl2  38039  ispridlc  38071  iss2  38333  membpartlem19  38810  paddasslem14  39834  ispsubcl2N  39948  cdleme29ex  40375  cdlemefr29exN  40403  eldiophss  42769  rencldnfilem  42815  oaabsb  43290  cantnfresb  43320  tfsconcatrn  43338  naddwordnexlem1  43393  clsk1indlem3  44039  ntrneikb  44090  mnuop3d  44267  ax6e2ndeq  44556  suctrALT2  44833  relpmin  44949  relpfrlem  44950  2reu3  47115  iccpartiltu  47427  bgoldbtbndlem2  47811  grtrimap  47951  grimgrtri  47952  isubgr3stgrlem6  47974  isubgr3stgr  47978  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem4  48113  itschlc0xyqsol1  48759  resipos  48967  elsetrecslem  49692  aacllem  49794