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  5217  f1oprg  5619  elovmporab1w  6212  cnvf1olem  6376  tfrcl  6516  nnaordi  6662  swoer  6716  0er  6722  pw2f1odclem  7003  mapxpen  7017  fict  7038  dif1enen  7050  php5fin  7052  fin0  7055  fin0or  7056  diffisn  7063  infnfi  7065  unsnfi  7092  fidcenumlemrk  7132  sbthlemi8  7142  fiuni  7156  supmoti  7171  eldju2ndl  7250  eldju2ndr  7251  omp1eomlem  7272  difinfsnlem  7277  ctmlemr  7286  nninfninc  7301  nninfwlpor  7352  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  enq0sym  7630  nqnq0pi  7636  addlocpr  7734  nqprl  7749  addnqprlemrl  7755  addnqprlemru  7756  mulnqprlemrl  7771  mulnqprlemru  7772  archpr  7841  cauappcvgprlemloc  7850  cauappcvgprlemladdfl  7853  archrecpr  7862  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprprlemml  7892  caucvgprprlemopl  7895  caucvgprprlemdisj  7900  caucvgprprlemloc  7901  suplocexprlemmu  7916  suplocexprlemdisj  7918  mulcmpblnrlemg  7938  caucvgsrlemgt1  7993  axarch  8089  axcaucvglemres  8097  cnegexlem2  8333  mulge0  8777  divdivap1  8881  divdivap2  8882  conjmulap  8887  ltdivmul  9034  nn0ge0div  9545  peano2uz2  9565  peano5uzti  9566  eluzp1m1  9758  xleadd1a  10081  iooshf  10160  divelunit  10210  eluzgtdifelfzo  10415  zsupcllemex  10462  ioom  10492  modqcyc2  10594  modaddmodup  10621  uzennn  10670  seq3fveq2  10709  seqfveq2g  10711  seq3id2  10760  seqfeq3  10763  expineg2  10782  mulexpzap  10813  leexp2r  10827  expnlbnd2  10899  hashfacen  11071  wrdred1hash  11128  ccatsymb  11150  swrdwrdsymbg  11211  swrdsb0eq  11212  ccatpfx  11248  swrdswrd  11252  wrdind  11269  wrd2ind  11270  swrdccatin1  11272  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12  11280  pfxccat3  11281  swrdccat  11282  resqrexlemp1rp  11532  resqrexlemfp1  11535  negfi  11754  climcaucn  11877  fsum3cvg3  11922  fsum2dlemstep  11960  mptfzshft  11968  expcnvre  12029  fprodrev  12145  fprod2dlemstep  12148  moddvds  12325  dvdsflip  12377  addmodlteqALT  12385  nn0o  12433  dfgcd2  12550  lcmgcdlem  12614  cncongr1  12640  prmind2  12657  isprm5lem  12678  isprm6  12684  cncongrprm  12694  oddpwdclemdc  12710  sqrt2irrap  12717  hashdvds  12758  crth  12761  prmdiveq  12773  hashgcdlem  12775  hashgcdeq  12777  pclem0  12824  pclemub  12825  pcprendvds2  12829  pcmul  12839  pcexp  12847  pcneg  12863  pc2dvds  12868  pcmpt  12881  prmpwdvds  12893  pockthg  12895  1arith  12905  4sqlem2  12927  4sqlemafi  12933  4sqlem11  12939  ennnfonelemex  13000  setscom  13087  subsubm  13531  insubm  13533  isgrpinv  13602  subsubg  13749  subsubrng  14193  subsubrg  14224  islss4  14361  znf1o  14630  znidomb  14637  tgcl  14753  lmbr2  14903  txcn  14964  txdis1cn  14967  txlm  14968  hmeoimaf1o  15003  txhmeo  15008  bl2in  15092  blssps  15116  blss  15117  blssexps  15118  blssex  15119  bdxmet  15190  xmetxp  15196  xmetxpbl  15197  xmettx  15199  metcnp3  15200  metcnpi3  15206  dedekindicc  15322  ivthdichlem  15340  limcimolemlt  15353  dvmptfsum  15414  rprelogbmul  15644  logbgcd1irr  15656  mpodvdsmulf1o  15679  lgsne0  15732  gausslemma2dlem1a  15752  lgseisenlem2  15765  lgsquadlemsfi  15769  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem2  15776  2sqlem8  15817  uspgredg2vlem  16033  iswlkg  16070  wlkl1loop  16099  upgriswlkdc  16101  clwwlkccatlem  16137  2omap  16418  qdencn  16455  trilpolemlt1  16469