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  1619  dfsb1  2481  unineq  4235  dfopif  4819  elssabg  5279  exopxfr2  5783  tz7.7  6332  oneqmini  6359  fvun1  6913  fconst5  7140  fpropnf1  7201  f1ounsn  7206  isomin  7271  isofrlem  7274  poxp  8058  poseq  8088  tposfo2  8179  onfununi  8261  tfrlem9a  8305  oecl  8452  oawordri  8465  omwordri  8487  odi  8494  pssnn  9078  prdom2  9897  acni2  9937  cardinfima  9988  cfslb2n  10159  infpssrlem4  10197  axdc3lem4  10344  brdom6disj  10423  tskr1om  10658  indpi  10798  1idpr  10920  1re  11112  mulge0  11635  infm3  12081  uzind  12565  suprfinzcl  12587  uzwo  12809  xrlttr  13039  xmullem2  13164  snunico  13379  fzen  13441  fz0fzelfz0  13534  sqlecan  14116  hashf1lem2  14363  ccatsymb  14490  lo1le  15559  fsumss  15632  ntrivcvgfvn0  15806  fprodss  15855  smupvallem  16394  zeqzmulgcd  16421  lcmgcdlem  16517  lcmdvds  16519  lcmfunsnlem2lem1  16549  coprmproddvdslem  16573  cncongr2  16579  exprmfct  16615  infpnlem1  16822  prmdvdsprmop  16955  prmgaplem7  16969  prmlem0  17017  sscfn2  17725  isssc  17727  iszeroi  17916  funcsetcestrclem8  18068  dirge  18509  efgval  19629  dmdprd  19912  dprdw  19924  rhmsubclem4  20603  lpigen  21272  psrbaglefi  21863  matvscl  22346  scmatghm  22448  slesolinv  22595  cpmatacl  22631  pnfnei  23135  mnfnei  23136  cmpcld  23317  isfildlem  23772  metrest  24439  blval2  24477  iscmet3lem2  25219  ivthlem3  25381  mbfi1fseqlem4  25646  itg2seq  25670  aalioulem6  26272  taylthlem2  26309  chpchtsum  27157  dchrmulcl  27187  bcmono  27215  nosupno  27642  nosupbday  27644  noinfno  27657  noinfbday  27659  nocvxminlem  27717  cuteq1  27778  onscutlt  28201  onsiso  28205  bdayn0p1  28294  zs12ge0  28393  cgrg3col4  28831  brbtwn2  28883  axeuclid  28941  umgredg  29116  pthdivtx  29705  pthdlem1  29744  shsvs  31303  cnlnssadj  32060  atexch  32361  mdsymlem5  32387  disjxpin  32568  fldextrspunlsplem  33686  sigaclci  34145  fnrelpredd  35102  satfv0  35402  satffunlem2lem1  35448  dmopab3rexdif  35449  elfuns  35957  altopth1  36007  btwnexch2  36065  ifscgr  36086  colinbtwnle  36160  trer  36358  elicc3  36359  bj-imdirval3  37226  bj-finsumval0  37327  difunieq  37416  fvineqsneu  37453  fvineqsneq  37454  poimirlem27  37695  poimir  37701  cnambfre  37716  itg2addnclem2  37720  itg2addnc  37722  areacirclem1  37756  heiborlem4  37862  elghomlem2OLD  37934  rngo2  37955  ispridl2  38086  ispridlc  38118  iss2  38380  membpartlem19  38857  paddasslem14  39880  ispsubcl2N  39994  cdleme29ex  40421  cdlemefr29exN  40449  eldiophss  42815  rencldnfilem  42861  oaabsb  43335  cantnfresb  43365  tfsconcatrn  43383  naddwordnexlem1  43438  clsk1indlem3  44084  ntrneikb  44135  mnuop3d  44312  ax6e2ndeq  44600  suctrALT2  44877  relpmin  44993  relpfrlem  44994  2reu3  47149  iccpartiltu  47461  bgoldbtbndlem2  47845  grtrimap  47987  grimgrtri  47988  isubgr3stgrlem6  48010  isubgr3stgr  48014  pgnbgreunbgrlem1  48152  pgnbgreunbgrlem4  48158  itschlc0xyqsol1  48806  resipos  49014  elsetrecslem  49739  aacllem  49841