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  1617  dfsb1  2485  unineq  4287  dfopif  4869  elssabg  5342  exopxfr2  5854  tz7.7  6409  oneqmini  6435  fvun1  6999  fconst5  7227  fpropnf1  7288  f1ounsn  7293  isomin  7358  isofrlem  7361  poxp  8154  poseq  8184  tposfo2  8275  onfununi  8382  tfrlem9a  8427  oecl  8576  oawordri  8589  omwordri  8611  odi  8618  pssnn  9209  prdom2  10047  acni2  10087  cardinfima  10138  cfslb2n  10309  infpssrlem4  10347  axdc3lem4  10494  brdom6disj  10573  tskr1om  10808  indpi  10948  1idpr  11070  1re  11262  mulge0  11782  infm3  12228  uzind  12712  suprfinzcl  12734  uzwo  12954  xrlttr  13183  xmullem2  13308  snunico  13520  fzen  13582  fz0fzelfz0  13675  sqlecan  14249  hashf1lem2  14496  ccatsymb  14621  lo1le  15689  fsumss  15762  ntrivcvgfvn0  15936  fprodss  15985  smupvallem  16521  zeqzmulgcd  16548  lcmgcdlem  16644  lcmdvds  16646  lcmfunsnlem2lem1  16676  coprmproddvdslem  16700  cncongr2  16706  exprmfct  16742  infpnlem1  16949  prmdvdsprmop  17082  prmgaplem7  17096  prmlem0  17144  sscfn2  17863  isssc  17865  iszeroi  18055  funcsetcestrclem8  18208  dirge  18649  efgval  19736  dmdprd  20019  dprdw  20031  rhmsubclem4  20689  lpigen  21346  psrbaglefi  21947  matvscl  22438  scmatghm  22540  slesolinv  22687  cpmatacl  22723  pnfnei  23229  mnfnei  23230  cmpcld  23411  isfildlem  23866  metrest  24538  blval2  24576  iscmet3lem2  25327  ivthlem3  25489  mbfi1fseqlem4  25754  itg2seq  25778  aalioulem6  26380  taylthlem2  26417  chpchtsum  27264  dchrmulcl  27294  bcmono  27322  nosupno  27749  nosupbday  27751  noinfno  27764  noinfbday  27766  nocvxminlem  27823  cuteq1  27879  cgrg3col4  28862  brbtwn2  28921  axeuclid  28979  umgredg  29156  pthdivtx  29748  pthdlem1  29787  shsvs  31343  cnlnssadj  32100  atexch  32401  mdsymlem5  32427  disjxpin  32602  fldextrspunlsplem  33724  sigaclci  34134  fnrelpredd  35104  satfv0  35364  satffunlem2lem1  35410  dmopab3rexdif  35411  elfuns  35917  altopth1  35967  btwnexch2  36025  ifscgr  36046  colinbtwnle  36120  trer  36318  elicc3  36319  bj-imdirval3  37186  bj-finsumval0  37287  difunieq  37376  fvineqsneu  37413  fvineqsneq  37414  poimirlem27  37655  poimir  37661  cnambfre  37676  itg2addnclem2  37680  itg2addnc  37682  areacirclem1  37716  heiborlem4  37822  elghomlem2OLD  37894  rngo2  37915  ispridl2  38046  ispridlc  38078  iss2  38346  membpartlem19  38813  paddasslem14  39836  ispsubcl2N  39950  cdleme29ex  40377  cdlemefr29exN  40405  eldiophss  42790  rencldnfilem  42836  oaabsb  43312  cantnfresb  43342  tfsconcatrn  43360  naddwordnexlem1  43415  clsk1indlem3  44061  ntrneikb  44112  mnuop3d  44295  ax6e2ndeq  44584  suctrALT2  44862  relpmin  44978  relpfrlem  44979  2reu3  47127  iccpartiltu  47414  bgoldbtbndlem2  47798  grtrimap  47920  grimgrtri  47921  isubgr3stgrlem6  47943  isubgr3stgr  47947  itschlc0xyqsol1  48692  resipos  48879  elsetrecslem  49273  aacllem  49375