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

This theorem is referenced by:  im2anan9  619  jaoa  952  prlem1  1051  cad0  1621  cad0OLD  1622  dfsb1  2485  unineq  4208  dfopifOLD  4798  elssabg  5255  exopxfr2  5742  tz7.7  6277  oneqmini  6302  fvun1  6841  fconst5  7063  fpropnf1  7121  isomin  7188  isofrlem  7191  poxp  7940  tposfo2  8036  onfununi  8143  tfrlem9a  8188  oecl  8329  oawordri  8343  omwordri  8365  odi  8372  pssnn  8913  pssnnOLD  8969  prdom2  9693  acni2  9733  cardinfima  9784  cfslb2n  9955  infpssrlem4  9993  axdc3lem4  10140  brdom6disj  10219  tskr1om  10454  indpi  10594  1idpr  10716  1re  10906  mulge0  11423  infm3  11864  uzind  12342  suprfinzcl  12365  uzwo  12580  xrlttr  12803  xmullem2  12928  snunico  13140  fzen  13202  fz0fzelfz0  13291  sqlecan  13853  hashf1lem2  14098  ccatsymb  14215  lo1le  15291  fsumss  15365  ntrivcvgfvn0  15539  fprodss  15586  smupvallem  16118  zeqzmulgcd  16145  lcmgcdlem  16239  lcmdvds  16241  lcmfunsnlem2lem1  16271  coprmproddvdslem  16295  cncongr2  16301  exprmfct  16337  infpnlem1  16539  prmdvdsprmop  16672  prmgaplem7  16686  prmlem0  16735  sscfn2  17447  isssc  17449  iszeroi  17640  funcsetcestrclem8  17795  dirge  18236  efgval  19238  dmdprd  19516  dprdw  19528  ringadd2  19729  lpigen  20440  psrbaglefi  21045  psrbaglefiOLD  21046  matvscl  21488  scmatghm  21590  slesolinv  21737  cpmatacl  21773  pnfnei  22279  mnfnei  22280  cmpcld  22461  isfildlem  22916  metrest  23586  blval2  23624  iscmet3lem2  24361  ivthlem3  24522  mbfi1fseqlem4  24788  itg2seq  24812  aalioulem6  25402  chpchtsum  26272  dchrmulcl  26302  bcmono  26330  cgrg3col4  27118  brbtwn2  27176  axeuclid  27234  umgredg  27411  pthdivtx  27998  pthdlem1  28035  shsvs  29586  cnlnssadj  30343  atexch  30644  mdsymlem5  30670  disjxpin  30828  sigaclci  32000  fnrelpredd  32961  satfv0  33220  satffunlem2lem1  33266  dmopab3rexdif  33267  poseq  33729  nosupno  33833  nosupbday  33835  noinfno  33848  noinfbday  33850  nocvxminlem  33899  elfuns  34144  altopth1  34194  btwnexch2  34252  ifscgr  34273  colinbtwnle  34347  trer  34432  elicc3  34433  bj-imdirval3  35282  bj-finsumval0  35383  difunieq  35472  fvineqsneu  35509  fvineqsneq  35510  poimirlem27  35731  poimir  35737  cnambfre  35752  itg2addnclem2  35756  itg2addnc  35758  areacirclem1  35792  heiborlem4  35899  elghomlem2OLD  35971  rngo2  35992  ispridl2  36123  ispridlc  36155  iss2  36406  paddasslem14  37774  ispsubcl2N  37888  cdleme29ex  38315  cdlemefr29exN  38343  eldiophss  40512  rencldnfilem  40558  clsk1indlem3  41542  ntrneikb  41593  mnuop3d  41778  ax6e2ndeq  42068  suctrALT2  42346  2reu3  44489  iccpartiltu  44762  bgoldbtbndlem2  45146  rhmsubclem4  45535  itschlc0xyqsol1  46000  elsetrecslem  46290  aacllem  46391