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  5225  f1oprg  5629  elovmporab1w  6223  cnvf1olem  6389  tfrcl  6530  nnaordi  6676  swoer  6730  0er  6736  modom  6994  pw2f1odclem  7020  mapxpen  7034  fict  7055  dif1enen  7069  php5fin  7071  fin0  7074  fin0or  7075  diffisn  7082  infnfi  7084  unsnfi  7111  fidcenumlemrk  7153  sbthlemi8  7163  fiuni  7177  supmoti  7192  eldju2ndl  7271  eldju2ndr  7272  omp1eomlem  7293  difinfsnlem  7298  ctmlemr  7307  nninfninc  7322  nninfwlpor  7373  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  enq0sym  7652  nqnq0pi  7658  addlocpr  7756  nqprl  7771  addnqprlemrl  7777  addnqprlemru  7778  mulnqprlemrl  7793  mulnqprlemru  7794  archpr  7863  cauappcvgprlemloc  7872  cauappcvgprlemladdfl  7875  archrecpr  7884  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprprlemml  7914  caucvgprprlemopl  7917  caucvgprprlemdisj  7922  caucvgprprlemloc  7923  suplocexprlemmu  7938  suplocexprlemdisj  7940  mulcmpblnrlemg  7960  caucvgsrlemgt1  8015  axarch  8111  axcaucvglemres  8119  cnegexlem2  8355  mulge0  8799  divdivap1  8903  divdivap2  8904  conjmulap  8909  ltdivmul  9056  nn0ge0div  9567  peano2uz2  9587  peano5uzti  9588  eluzp1m1  9780  xleadd1a  10108  iooshf  10187  divelunit  10237  eluzgtdifelfzo  10443  zsupcllemex  10491  ioom  10521  modqcyc2  10623  modaddmodup  10650  uzennn  10699  seq3fveq2  10738  seqfveq2g  10740  seq3id2  10789  seqfeq3  10792  expineg2  10811  mulexpzap  10842  leexp2r  10856  expnlbnd2  10928  hashfacen  11101  wrdred1hash  11161  ccatsymb  11183  swrdwrdsymbg  11249  swrdsb0eq  11250  ccatpfx  11286  swrdswrd  11290  wrdind  11307  wrd2ind  11308  swrdccatin1  11310  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  resqrexlemp1rp  11584  resqrexlemfp1  11587  negfi  11806  climcaucn  11929  fsum3cvg3  11975  fsum2dlemstep  12013  mptfzshft  12021  expcnvre  12082  fprodrev  12198  fprod2dlemstep  12201  moddvds  12378  dvdsflip  12430  addmodlteqALT  12438  nn0o  12486  dfgcd2  12603  lcmgcdlem  12667  cncongr1  12693  prmind2  12710  isprm5lem  12731  isprm6  12737  cncongrprm  12747  oddpwdclemdc  12763  sqrt2irrap  12770  hashdvds  12811  crth  12814  prmdiveq  12826  hashgcdlem  12828  hashgcdeq  12830  pclem0  12877  pclemub  12878  pcprendvds2  12882  pcmul  12892  pcexp  12900  pcneg  12916  pc2dvds  12921  pcmpt  12934  prmpwdvds  12946  pockthg  12948  1arith  12958  4sqlem2  12980  4sqlemafi  12986  4sqlem11  12992  ennnfonelemex  13053  setscom  13140  subsubm  13584  insubm  13586  isgrpinv  13655  subsubg  13802  subsubrng  14247  subsubrg  14278  islss4  14415  znf1o  14684  znidomb  14691  tgcl  14807  lmbr2  14957  txcn  15018  txdis1cn  15021  txlm  15022  hmeoimaf1o  15057  txhmeo  15062  bl2in  15146  blssps  15170  blss  15171  blssexps  15172  blssex  15173  bdxmet  15244  xmetxp  15250  xmetxpbl  15251  xmettx  15253  metcnp3  15254  metcnpi3  15260  dedekindicc  15376  ivthdichlem  15394  limcimolemlt  15407  dvmptfsum  15468  rprelogbmul  15698  logbgcd1irr  15710  mpodvdsmulf1o  15733  lgsne0  15786  gausslemma2dlem1a  15806  lgseisenlem2  15819  lgsquadlemsfi  15823  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem2  15830  2sqlem8  15871  uspgredg2vlem  16090  subuhgr  16142  subupgr  16143  subumgr  16144  iswlkg  16199  wlkl1loop  16228  upgriswlkdc  16230  clwwlkccatlem  16270  clwwlkn1loopb  16290  clwwlknonex2e  16310  2omap  16645  qdencn  16682  trilpolemlt1  16696