Theorem ad2antrl 490

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad2antrl	⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

Proof of Theorem ad2antrl

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantl 277	1 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simprl  529  simprll  537  simprlr  538  elxp5  5216  f1oprg  5616  elovmporab1w  6205  cnvf1olem  6368  tfrcl  6508  nnaordi  6652  swoer  6706  0er  6712  pw2f1odclem  6991  mapxpen  7005  fict  7026  dif1enen  7038  php5fin  7040  fin0  7043  fin0or  7044  diffisn  7051  infnfi  7053  unsnfi  7077  fidcenumlemrk  7117  sbthlemi8  7127  fiuni  7141  supmoti  7156  eldju2ndl  7235  eldju2ndr  7236  omp1eomlem  7257  difinfsnlem  7262  ctmlemr  7271  nninfninc  7286  nninfwlpor  7337  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  enq0sym  7615  nqnq0pi  7621  addlocpr  7719  nqprl  7734  addnqprlemrl  7740  addnqprlemru  7741  mulnqprlemrl  7756  mulnqprlemru  7757  archpr  7826  cauappcvgprlemloc  7835  cauappcvgprlemladdfl  7838  archrecpr  7847  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprprlemml  7877  caucvgprprlemopl  7880  caucvgprprlemdisj  7885  caucvgprprlemloc  7886  suplocexprlemmu  7901  suplocexprlemdisj  7903  mulcmpblnrlemg  7923  caucvgsrlemgt1  7978  axarch  8074  axcaucvglemres  8082  cnegexlem2  8318  mulge0  8762  divdivap1  8866  divdivap2  8867  conjmulap  8872  ltdivmul  9019  nn0ge0div  9530  peano2uz2  9550  peano5uzti  9551  eluzp1m1  9742  xleadd1a  10065  iooshf  10144  divelunit  10194  eluzgtdifelfzo  10398  zsupcllemex  10445  ioom  10475  modqcyc2  10577  modaddmodup  10604  uzennn  10653  seq3fveq2  10692  seqfveq2g  10694  seq3id2  10743  seqfeq3  10746  expineg2  10765  mulexpzap  10796  leexp2r  10810  expnlbnd2  10882  hashfacen  11053  wrdred1hash  11110  ccatsymb  11132  swrdwrdsymbg  11191  swrdsb0eq  11192  ccatpfx  11228  swrdswrd  11232  wrdind  11249  wrd2ind  11250  swrdccatin1  11252  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12  11260  pfxccat3  11261  swrdccat  11262  resqrexlemp1rp  11512  resqrexlemfp1  11515  negfi  11734  climcaucn  11857  fsum3cvg3  11902  fsum2dlemstep  11940  mptfzshft  11948  expcnvre  12009  fprodrev  12125  fprod2dlemstep  12128  moddvds  12305  dvdsflip  12357  addmodlteqALT  12365  nn0o  12413  dfgcd2  12530  lcmgcdlem  12594  cncongr1  12620  prmind2  12637  isprm5lem  12658  isprm6  12664  cncongrprm  12674  oddpwdclemdc  12690  sqrt2irrap  12697  hashdvds  12738  crth  12741  prmdiveq  12753  hashgcdlem  12755  hashgcdeq  12757  pclem0  12804  pclemub  12805  pcprendvds2  12809  pcmul  12819  pcexp  12827  pcneg  12843  pc2dvds  12848  pcmpt  12861  prmpwdvds  12873  pockthg  12875  1arith  12885  4sqlem2  12907  4sqlemafi  12913  4sqlem11  12919  ennnfonelemex  12980  setscom  13067  subsubm  13511  insubm  13513  isgrpinv  13582  subsubg  13729  subsubrng  14172  subsubrg  14203  islss4  14340  znf1o  14609  znidomb  14616  tgcl  14732  lmbr2  14882  txcn  14943  txdis1cn  14946  txlm  14947  hmeoimaf1o  14982  txhmeo  14987  bl2in  15071  blssps  15095  blss  15096  blssexps  15097  blssex  15098  bdxmet  15169  xmetxp  15175  xmetxpbl  15176  xmettx  15178  metcnp3  15179  metcnpi3  15185  dedekindicc  15301  ivthdichlem  15319  limcimolemlt  15332  dvmptfsum  15393  rprelogbmul  15623  logbgcd1irr  15635  mpodvdsmulf1o  15658  lgsne0  15711  gausslemma2dlem1a  15731  lgseisenlem2  15744  lgsquadlemsfi  15748  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2lem2  15755  2sqlem8  15796  uspgredg2vlem  16012  iswlkg  16032  2omap  16318  qdencn  16354  trilpolemlt1  16368