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  5170  f1oprg  5565  elovmporab1w  6146  cnvf1olem  6309  tfrcl  6449  nnaordi  6593  swoer  6647  0er  6653  pw2f1odclem  6930  mapxpen  6944  fict  6964  dif1enen  6976  php5fin  6978  fin0  6981  fin0or  6982  diffisn  6989  infnfi  6991  unsnfi  7015  fidcenumlemrk  7055  sbthlemi8  7065  fiuni  7079  supmoti  7094  eldju2ndl  7173  eldju2ndr  7174  omp1eomlem  7195  difinfsnlem  7200  ctmlemr  7209  nninfninc  7224  nninfwlpor  7275  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  enq0sym  7544  nqnq0pi  7550  addlocpr  7648  nqprl  7663  addnqprlemrl  7669  addnqprlemru  7670  mulnqprlemrl  7685  mulnqprlemru  7686  archpr  7755  cauappcvgprlemloc  7764  cauappcvgprlemladdfl  7767  archrecpr  7776  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprprlemml  7806  caucvgprprlemopl  7809  caucvgprprlemdisj  7814  caucvgprprlemloc  7815  suplocexprlemmu  7830  suplocexprlemdisj  7832  mulcmpblnrlemg  7852  caucvgsrlemgt1  7907  axarch  8003  axcaucvglemres  8011  cnegexlem2  8247  mulge0  8691  divdivap1  8795  divdivap2  8796  conjmulap  8801  ltdivmul  8948  nn0ge0div  9459  peano2uz2  9479  peano5uzti  9480  eluzp1m1  9671  xleadd1a  9994  iooshf  10073  divelunit  10123  eluzgtdifelfzo  10324  zsupcllemex  10371  ioom  10401  modqcyc2  10503  modaddmodup  10530  uzennn  10579  seq3fveq2  10618  seqfveq2g  10620  seq3id2  10669  seqfeq3  10672  expineg2  10691  mulexpzap  10722  leexp2r  10736  expnlbnd2  10808  hashfacen  10979  wrdred1hash  11035  ccatsymb  11056  resqrexlemp1rp  11288  resqrexlemfp1  11291  negfi  11510  climcaucn  11633  fsum3cvg3  11678  fsum2dlemstep  11716  mptfzshft  11724  expcnvre  11785  fprodrev  11901  fprod2dlemstep  11904  moddvds  12081  dvdsflip  12133  addmodlteqALT  12141  nn0o  12189  dfgcd2  12306  lcmgcdlem  12370  cncongr1  12396  prmind2  12413  isprm5lem  12434  isprm6  12440  cncongrprm  12450  oddpwdclemdc  12466  sqrt2irrap  12473  hashdvds  12514  crth  12517  prmdiveq  12529  hashgcdlem  12531  hashgcdeq  12533  pclem0  12580  pclemub  12581  pcprendvds2  12585  pcmul  12595  pcexp  12603  pcneg  12619  pc2dvds  12624  pcmpt  12637  prmpwdvds  12649  pockthg  12651  1arith  12661  4sqlem2  12683  4sqlemafi  12689  4sqlem11  12695  ennnfonelemex  12756  setscom  12843  subsubm  13286  insubm  13288  isgrpinv  13357  subsubg  13504  subsubrng  13947  subsubrg  13978  islss4  14115  znf1o  14384  znidomb  14391  tgcl  14507  lmbr2  14657  txcn  14718  txdis1cn  14721  txlm  14722  hmeoimaf1o  14757  txhmeo  14762  bl2in  14846  blssps  14870  blss  14871  blssexps  14872  blssex  14873  bdxmet  14944  xmetxp  14950  xmetxpbl  14951  xmettx  14953  metcnp3  14954  metcnpi3  14960  dedekindicc  15076  ivthdichlem  15094  limcimolemlt  15107  dvmptfsum  15168  rprelogbmul  15398  logbgcd1irr  15410  mpodvdsmulf1o  15433  lgsne0  15486  gausslemma2dlem1a  15506  lgseisenlem2  15519  lgsquadlemsfi  15523  lgsquadlem1  15525  lgsquadlem2  15526  lgsquadlem3  15527  lgsquad2lem2  15530  2sqlem8  15571  2omap  15894  qdencn  15928  trilpolemlt1  15942