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  531  simprll  539  simprlr  540  elxp5  5232  f1oprg  5638  elovmporab1w  6233  cnvf1olem  6398  ressuppss  6432  tfrcl  6573  nnaordi  6719  swoer  6773  0er  6779  modom  7037  pw2f1odclem  7063  mapxpen  7077  fict  7098  dif1enen  7112  php5fin  7114  fin0  7117  fin0or  7118  diffisn  7125  infnfi  7127  unsnfi  7154  fidcenumlemrk  7196  sbthlemi8  7206  fiuni  7220  supmoti  7235  eldju2ndl  7314  eldju2ndr  7315  omp1eomlem  7336  difinfsnlem  7341  ctmlemr  7350  nninfninc  7365  nninfwlpor  7416  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  enq0sym  7695  nqnq0pi  7701  addlocpr  7799  nqprl  7814  addnqprlemrl  7820  addnqprlemru  7821  mulnqprlemrl  7836  mulnqprlemru  7837  archpr  7906  cauappcvgprlemloc  7915  cauappcvgprlemladdfl  7918  archrecpr  7927  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprprlemml  7957  caucvgprprlemopl  7960  caucvgprprlemdisj  7965  caucvgprprlemloc  7966  suplocexprlemmu  7981  suplocexprlemdisj  7983  mulcmpblnrlemg  8003  caucvgsrlemgt1  8058  axarch  8154  axcaucvglemres  8162  cnegexlem2  8397  mulge0  8841  divdivap1  8945  divdivap2  8946  conjmulap  8951  ltdivmul  9098  nn0ge0div  9611  peano2uz2  9631  peano5uzti  9632  eluzp1m1  9824  xleadd1a  10152  iooshf  10231  divelunit  10281  eluzgtdifelfzo  10488  zsupcllemex  10536  ioom  10566  modqcyc2  10668  modaddmodup  10695  uzennn  10744  seq3fveq2  10783  seqfveq2g  10785  seq3id2  10834  seqfeq3  10837  expineg2  10856  mulexpzap  10887  leexp2r  10901  expnlbnd2  10973  hashfacen  11146  wrdred1hash  11206  ccatsymb  11228  swrdwrdsymbg  11294  swrdsb0eq  11295  ccatpfx  11331  swrdswrd  11335  wrdind  11352  wrd2ind  11353  swrdccatin1  11355  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12  11363  pfxccat3  11364  swrdccat  11365  resqrexlemp1rp  11629  resqrexlemfp1  11632  negfi  11851  climcaucn  11974  fsum3cvg3  12020  fsum2dlemstep  12058  mptfzshft  12066  expcnvre  12127  fprodrev  12243  fprod2dlemstep  12246  moddvds  12423  dvdsflip  12475  addmodlteqALT  12483  nn0o  12531  dfgcd2  12648  lcmgcdlem  12712  cncongr1  12738  prmind2  12755  isprm5lem  12776  isprm6  12782  cncongrprm  12792  oddpwdclemdc  12808  sqrt2irrap  12815  hashdvds  12856  crth  12859  prmdiveq  12871  hashgcdlem  12873  hashgcdeq  12875  pclem0  12922  pclemub  12923  pcprendvds2  12927  pcmul  12937  pcexp  12945  pcneg  12961  pc2dvds  12966  pcmpt  12979  prmpwdvds  12991  pockthg  12993  1arith  13003  4sqlem2  13025  4sqlemafi  13031  4sqlem11  13037  ennnfonelemex  13098  setscom  13185  subsubm  13629  insubm  13631  isgrpinv  13700  subsubg  13847  subsubrng  14292  subsubrg  14323  islss4  14461  znf1o  14730  znidomb  14737  tgcl  14858  lmbr2  15008  txcn  15069  txdis1cn  15072  txlm  15073  hmeoimaf1o  15108  txhmeo  15113  bl2in  15197  blssps  15221  blss  15222  blssexps  15223  blssex  15224  bdxmet  15295  xmetxp  15301  xmetxpbl  15302  xmettx  15304  metcnp3  15305  metcnpi3  15311  dedekindicc  15427  ivthdichlem  15445  limcimolemlt  15458  dvmptfsum  15519  rprelogbmul  15749  logbgcd1irr  15761  mpodvdsmulf1o  15787  lgsne0  15840  gausslemma2dlem1a  15860  lgseisenlem2  15873  lgsquadlemsfi  15877  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2lem2  15884  2sqlem8  15925  uspgredg2vlem  16144  subuhgr  16196  subupgr  16197  subumgr  16198  iswlkg  16253  wlkl1loop  16282  upgriswlkdc  16284  clwwlkccatlem  16324  clwwlkn1loopb  16344  clwwlknonex2e  16364  2omap  16698  qdencn  16738  trilpolemlt1  16756