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  7283  exmidfodomrlemrALT  7284  enq0sym  7518  nqnq0pi  7524  addlocpr  7622  nqprl  7637  addnqprlemrl  7643  addnqprlemru  7644  mulnqprlemrl  7659  mulnqprlemru  7660  archpr  7729  cauappcvgprlemloc  7738  cauappcvgprlemladdfl  7741  archrecpr  7750  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprprlemml  7780  caucvgprprlemopl  7783  caucvgprprlemdisj  7788  caucvgprprlemloc  7789  suplocexprlemmu  7804  suplocexprlemdisj  7806  mulcmpblnrlemg  7826  caucvgsrlemgt1  7881  axarch  7977  axcaucvglemres  7985  cnegexlem2  8221  mulge0  8665  divdivap1  8769  divdivap2  8770  conjmulap  8775  ltdivmul  8922  nn0ge0div  9432  peano2uz2  9452  peano5uzti  9453  eluzp1m1  9644  xleadd1a  9967  iooshf  10046  divelunit  10096  eluzgtdifelfzo  10292  zsupcllemex  10339  ioom  10369  modqcyc2  10471  modaddmodup  10498  uzennn  10547  seq3fveq2  10586  seqfveq2g  10588  seq3id2  10637  seqfeq3  10640  expineg2  10659  mulexpzap  10690  leexp2r  10704  expnlbnd2  10776  hashfacen  10947  wrdred1hash  10997  resqrexlemp1rp  11190  resqrexlemfp1  11193  negfi  11412  climcaucn  11535  fsum3cvg3  11580  fsum2dlemstep  11618  mptfzshft  11626  expcnvre  11687  fprodrev  11803  fprod2dlemstep  11806  moddvds  11983  dvdsflip  12035  addmodlteqALT  12043  nn0o  12091  dfgcd2  12208  lcmgcdlem  12272  cncongr1  12298  prmind2  12315  isprm5lem  12336  isprm6  12342  cncongrprm  12352  oddpwdclemdc  12368  sqrt2irrap  12375  hashdvds  12416  crth  12419  prmdiveq  12431  hashgcdlem  12433  hashgcdeq  12435  pclem0  12482  pclemub  12483  pcprendvds2  12487  pcmul  12497  pcexp  12505  pcneg  12521  pc2dvds  12526  pcmpt  12539  prmpwdvds  12551  pockthg  12553  1arith  12563  4sqlem2  12585  4sqlemafi  12591  4sqlem11  12597  ennnfonelemex  12658  setscom  12745  subsubm  13187  insubm  13189  isgrpinv  13258  subsubg  13405  subsubrng  13848  subsubrg  13879  islss4  14016  znf1o  14285  znidomb  14292  tgcl  14408  lmbr2  14558  txcn  14619  txdis1cn  14622  txlm  14623  hmeoimaf1o  14658  txhmeo  14663  bl2in  14747  blssps  14771  blss  14772  blssexps  14773  blssex  14774  bdxmet  14845  xmetxp  14851  xmetxpbl  14852  xmettx  14854  metcnp3  14855  metcnpi3  14861  dedekindicc  14977  ivthdichlem  14995  limcimolemlt  15008  dvmptfsum  15069  rprelogbmul  15299  logbgcd1irr  15311  mpodvdsmulf1o  15334  lgsne0  15387  gausslemma2dlem1a  15407  lgseisenlem2  15420  lgsquadlemsfi  15424  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad2lem2  15431  2sqlem8  15472  2omap  15750  qdencn  15784  trilpolemlt1  15798