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  5159  f1oprg  5551  elovmporab1w  6128  cnvf1olem  6291  tfrcl  6431  nnaordi  6575  swoer  6629  0er  6635  pw2f1odclem  6904  mapxpen  6918  fict  6938  dif1enen  6950  php5fin  6952  fin0  6955  fin0or  6956  diffisn  6963  infnfi  6965  unsnfi  6989  fidcenumlemrk  7029  sbthlemi8  7039  fiuni  7053  supmoti  7068  eldju2ndl  7147  eldju2ndr  7148  omp1eomlem  7169  difinfsnlem  7174  ctmlemr  7183  nninfninc  7198  nninfwlpor  7249  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  enq0sym  7516  nqnq0pi  7522  addlocpr  7620  nqprl  7635  addnqprlemrl  7641  addnqprlemru  7642  mulnqprlemrl  7657  mulnqprlemru  7658  archpr  7727  cauappcvgprlemloc  7736  cauappcvgprlemladdfl  7739  archrecpr  7748  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprprlemml  7778  caucvgprprlemopl  7781  caucvgprprlemdisj  7786  caucvgprprlemloc  7787  suplocexprlemmu  7802  suplocexprlemdisj  7804  mulcmpblnrlemg  7824  caucvgsrlemgt1  7879  axarch  7975  axcaucvglemres  7983  cnegexlem2  8219  mulge0  8663  divdivap1  8767  divdivap2  8768  conjmulap  8773  ltdivmul  8920  nn0ge0div  9430  peano2uz2  9450  peano5uzti  9451  eluzp1m1  9642  xleadd1a  9965  iooshf  10044  divelunit  10094  eluzgtdifelfzo  10290  zsupcllemex  10337  ioom  10367  modqcyc2  10469  modaddmodup  10496  uzennn  10545  seq3fveq2  10584  seqfveq2g  10586  seq3id2  10635  seqfeq3  10638  expineg2  10657  mulexpzap  10688  leexp2r  10702  expnlbnd2  10774  hashfacen  10945  wrdred1hash  10995  resqrexlemp1rp  11188  resqrexlemfp1  11191  negfi  11410  climcaucn  11533  fsum3cvg3  11578  fsum2dlemstep  11616  mptfzshft  11624  expcnvre  11685  fprodrev  11801  fprod2dlemstep  11804  moddvds  11981  dvdsflip  12033  addmodlteqALT  12041  nn0o  12089  dfgcd2  12206  lcmgcdlem  12270  cncongr1  12296  prmind2  12313  isprm5lem  12334  isprm6  12340  cncongrprm  12350  oddpwdclemdc  12366  sqrt2irrap  12373  hashdvds  12414  crth  12417  prmdiveq  12429  hashgcdlem  12431  hashgcdeq  12433  pclem0  12480  pclemub  12481  pcprendvds2  12485  pcmul  12495  pcexp  12503  pcneg  12519  pc2dvds  12524  pcmpt  12537  prmpwdvds  12549  pockthg  12551  1arith  12561  4sqlem2  12583  4sqlemafi  12589  4sqlem11  12595  ennnfonelemex  12656  setscom  12743  subsubm  13185  insubm  13187  isgrpinv  13256  subsubg  13403  subsubrng  13846  subsubrg  13877  islss4  14014  znf1o  14283  znidomb  14290  tgcl  14384  lmbr2  14534  txcn  14595  txdis1cn  14598  txlm  14599  hmeoimaf1o  14634  txhmeo  14639  bl2in  14723  blssps  14747  blss  14748  blssexps  14749  blssex  14750  bdxmet  14821  xmetxp  14827  xmetxpbl  14828  xmettx  14830  metcnp3  14831  metcnpi3  14837  dedekindicc  14953  ivthdichlem  14971  limcimolemlt  14984  dvmptfsum  15045  rprelogbmul  15275  logbgcd1irr  15287  mpodvdsmulf1o  15310  lgsne0  15363  gausslemma2dlem1a  15383  lgseisenlem2  15396  lgsquadlemsfi  15400  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem2  15407  2sqlem8  15448  2omap  15726  qdencn  15758  trilpolemlt1  15772