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  5223  f1oprg  5625  elovmporab1w  6218  cnvf1olem  6384  tfrcl  6525  nnaordi  6671  swoer  6725  0er  6731  modom  6989  pw2f1odclem  7015  mapxpen  7029  fict  7050  dif1enen  7062  php5fin  7064  fin0  7067  fin0or  7068  diffisn  7075  infnfi  7077  unsnfi  7104  fidcenumlemrk  7144  sbthlemi8  7154  fiuni  7168  supmoti  7183  eldju2ndl  7262  eldju2ndr  7263  omp1eomlem  7284  difinfsnlem  7289  ctmlemr  7298  nninfninc  7313  nninfwlpor  7364  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  enq0sym  7642  nqnq0pi  7648  addlocpr  7746  nqprl  7761  addnqprlemrl  7767  addnqprlemru  7768  mulnqprlemrl  7783  mulnqprlemru  7784  archpr  7853  cauappcvgprlemloc  7862  cauappcvgprlemladdfl  7865  archrecpr  7874  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprprlemml  7904  caucvgprprlemopl  7907  caucvgprprlemdisj  7912  caucvgprprlemloc  7913  suplocexprlemmu  7928  suplocexprlemdisj  7930  mulcmpblnrlemg  7950  caucvgsrlemgt1  8005  axarch  8101  axcaucvglemres  8109  cnegexlem2  8345  mulge0  8789  divdivap1  8893  divdivap2  8894  conjmulap  8899  ltdivmul  9046  nn0ge0div  9557  peano2uz2  9577  peano5uzti  9578  eluzp1m1  9770  xleadd1a  10098  iooshf  10177  divelunit  10227  eluzgtdifelfzo  10432  zsupcllemex  10480  ioom  10510  modqcyc2  10612  modaddmodup  10639  uzennn  10688  seq3fveq2  10727  seqfveq2g  10729  seq3id2  10778  seqfeq3  10781  expineg2  10800  mulexpzap  10831  leexp2r  10845  expnlbnd2  10917  hashfacen  11090  wrdred1hash  11147  ccatsymb  11169  swrdwrdsymbg  11235  swrdsb0eq  11236  ccatpfx  11272  swrdswrd  11276  wrdind  11293  wrd2ind  11294  swrdccatin1  11296  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12  11304  pfxccat3  11305  swrdccat  11306  resqrexlemp1rp  11557  resqrexlemfp1  11560  negfi  11779  climcaucn  11902  fsum3cvg3  11947  fsum2dlemstep  11985  mptfzshft  11993  expcnvre  12054  fprodrev  12170  fprod2dlemstep  12173  moddvds  12350  dvdsflip  12402  addmodlteqALT  12410  nn0o  12458  dfgcd2  12575  lcmgcdlem  12639  cncongr1  12665  prmind2  12682  isprm5lem  12703  isprm6  12709  cncongrprm  12719  oddpwdclemdc  12735  sqrt2irrap  12742  hashdvds  12783  crth  12786  prmdiveq  12798  hashgcdlem  12800  hashgcdeq  12802  pclem0  12849  pclemub  12850  pcprendvds2  12854  pcmul  12864  pcexp  12872  pcneg  12888  pc2dvds  12893  pcmpt  12906  prmpwdvds  12918  pockthg  12920  1arith  12930  4sqlem2  12952  4sqlemafi  12958  4sqlem11  12964  ennnfonelemex  13025  setscom  13112  subsubm  13556  insubm  13558  isgrpinv  13627  subsubg  13774  subsubrng  14218  subsubrg  14249  islss4  14386  znf1o  14655  znidomb  14662  tgcl  14778  lmbr2  14928  txcn  14989  txdis1cn  14992  txlm  14993  hmeoimaf1o  15028  txhmeo  15033  bl2in  15117  blssps  15141  blss  15142  blssexps  15143  blssex  15144  bdxmet  15215  xmetxp  15221  xmetxpbl  15222  xmettx  15224  metcnp3  15225  metcnpi3  15231  dedekindicc  15347  ivthdichlem  15365  limcimolemlt  15378  dvmptfsum  15439  rprelogbmul  15669  logbgcd1irr  15681  mpodvdsmulf1o  15704  lgsne0  15757  gausslemma2dlem1a  15777  lgseisenlem2  15790  lgsquadlemsfi  15794  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem2  15801  2sqlem8  15842  uspgredg2vlem  16059  iswlkg  16126  wlkl1loop  16155  upgriswlkdc  16157  clwwlkccatlem  16195  clwwlkn1loopb  16215  clwwlknonex2e  16235  2omap  16530  qdencn  16567  trilpolemlt1  16581