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  5171  f1oprg  5566  elovmporab1w  6147  cnvf1olem  6310  tfrcl  6450  nnaordi  6594  swoer  6648  0er  6654  pw2f1odclem  6931  mapxpen  6945  fict  6965  dif1enen  6977  php5fin  6979  fin0  6982  fin0or  6983  diffisn  6990  infnfi  6992  unsnfi  7016  fidcenumlemrk  7056  sbthlemi8  7066  fiuni  7080  supmoti  7095  eldju2ndl  7174  eldju2ndr  7175  omp1eomlem  7196  difinfsnlem  7201  ctmlemr  7210  nninfninc  7225  nninfwlpor  7276  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  enq0sym  7545  nqnq0pi  7551  addlocpr  7649  nqprl  7664  addnqprlemrl  7670  addnqprlemru  7671  mulnqprlemrl  7686  mulnqprlemru  7687  archpr  7756  cauappcvgprlemloc  7765  cauappcvgprlemladdfl  7768  archrecpr  7777  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprprlemml  7807  caucvgprprlemopl  7810  caucvgprprlemdisj  7815  caucvgprprlemloc  7816  suplocexprlemmu  7831  suplocexprlemdisj  7833  mulcmpblnrlemg  7853  caucvgsrlemgt1  7908  axarch  8004  axcaucvglemres  8012  cnegexlem2  8248  mulge0  8692  divdivap1  8796  divdivap2  8797  conjmulap  8802  ltdivmul  8949  nn0ge0div  9460  peano2uz2  9480  peano5uzti  9481  eluzp1m1  9672  xleadd1a  9995  iooshf  10074  divelunit  10124  eluzgtdifelfzo  10326  zsupcllemex  10373  ioom  10403  modqcyc2  10505  modaddmodup  10532  uzennn  10581  seq3fveq2  10620  seqfveq2g  10622  seq3id2  10671  seqfeq3  10674  expineg2  10693  mulexpzap  10724  leexp2r  10738  expnlbnd2  10810  hashfacen  10981  wrdred1hash  11037  ccatsymb  11058  swrdwrdsymbg  11117  swrdsb0eq  11118  resqrexlemp1rp  11317  resqrexlemfp1  11320  negfi  11539  climcaucn  11662  fsum3cvg3  11707  fsum2dlemstep  11745  mptfzshft  11753  expcnvre  11814  fprodrev  11930  fprod2dlemstep  11933  moddvds  12110  dvdsflip  12162  addmodlteqALT  12170  nn0o  12218  dfgcd2  12335  lcmgcdlem  12399  cncongr1  12425  prmind2  12442  isprm5lem  12463  isprm6  12469  cncongrprm  12479  oddpwdclemdc  12495  sqrt2irrap  12502  hashdvds  12543  crth  12546  prmdiveq  12558  hashgcdlem  12560  hashgcdeq  12562  pclem0  12609  pclemub  12610  pcprendvds2  12614  pcmul  12624  pcexp  12632  pcneg  12648  pc2dvds  12653  pcmpt  12666  prmpwdvds  12678  pockthg  12680  1arith  12690  4sqlem2  12712  4sqlemafi  12718  4sqlem11  12724  ennnfonelemex  12785  setscom  12872  subsubm  13315  insubm  13317  isgrpinv  13386  subsubg  13533  subsubrng  13976  subsubrg  14007  islss4  14144  znf1o  14413  znidomb  14420  tgcl  14536  lmbr2  14686  txcn  14747  txdis1cn  14750  txlm  14751  hmeoimaf1o  14786  txhmeo  14791  bl2in  14875  blssps  14899  blss  14900  blssexps  14901  blssex  14902  bdxmet  14973  xmetxp  14979  xmetxpbl  14980  xmettx  14982  metcnp3  14983  metcnpi3  14989  dedekindicc  15105  ivthdichlem  15123  limcimolemlt  15136  dvmptfsum  15197  rprelogbmul  15427  logbgcd1irr  15439  mpodvdsmulf1o  15462  lgsne0  15515  gausslemma2dlem1a  15535  lgseisenlem2  15548  lgsquadlemsfi  15552  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad2lem2  15559  2sqlem8  15600  2omap  15932  qdencn  15966  trilpolemlt1  15980