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  5190  f1oprg  5589  elovmporab1w  6170  cnvf1olem  6333  tfrcl  6473  nnaordi  6617  swoer  6671  0er  6677  pw2f1odclem  6956  mapxpen  6970  fict  6991  dif1enen  7003  php5fin  7005  fin0  7008  fin0or  7009  diffisn  7016  infnfi  7018  unsnfi  7042  fidcenumlemrk  7082  sbthlemi8  7092  fiuni  7106  supmoti  7121  eldju2ndl  7200  eldju2ndr  7201  omp1eomlem  7222  difinfsnlem  7227  ctmlemr  7236  nninfninc  7251  nninfwlpor  7302  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  enq0sym  7580  nqnq0pi  7586  addlocpr  7684  nqprl  7699  addnqprlemrl  7705  addnqprlemru  7706  mulnqprlemrl  7721  mulnqprlemru  7722  archpr  7791  cauappcvgprlemloc  7800  cauappcvgprlemladdfl  7803  archrecpr  7812  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprprlemml  7842  caucvgprprlemopl  7845  caucvgprprlemdisj  7850  caucvgprprlemloc  7851  suplocexprlemmu  7866  suplocexprlemdisj  7868  mulcmpblnrlemg  7888  caucvgsrlemgt1  7943  axarch  8039  axcaucvglemres  8047  cnegexlem2  8283  mulge0  8727  divdivap1  8831  divdivap2  8832  conjmulap  8837  ltdivmul  8984  nn0ge0div  9495  peano2uz2  9515  peano5uzti  9516  eluzp1m1  9707  xleadd1a  10030  iooshf  10109  divelunit  10159  eluzgtdifelfzo  10363  zsupcllemex  10410  ioom  10440  modqcyc2  10542  modaddmodup  10569  uzennn  10618  seq3fveq2  10657  seqfveq2g  10659  seq3id2  10708  seqfeq3  10711  expineg2  10730  mulexpzap  10761  leexp2r  10775  expnlbnd2  10847  hashfacen  11018  wrdred1hash  11074  ccatsymb  11096  swrdwrdsymbg  11155  swrdsb0eq  11156  ccatpfx  11192  swrdswrd  11196  wrdind  11213  wrd2ind  11214  swrdccatin1  11216  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12  11224  pfxccat3  11225  swrdccat  11226  resqrexlemp1rp  11432  resqrexlemfp1  11435  negfi  11654  climcaucn  11777  fsum3cvg3  11822  fsum2dlemstep  11860  mptfzshft  11868  expcnvre  11929  fprodrev  12045  fprod2dlemstep  12048  moddvds  12225  dvdsflip  12277  addmodlteqALT  12285  nn0o  12333  dfgcd2  12450  lcmgcdlem  12514  cncongr1  12540  prmind2  12557  isprm5lem  12578  isprm6  12584  cncongrprm  12594  oddpwdclemdc  12610  sqrt2irrap  12617  hashdvds  12658  crth  12661  prmdiveq  12673  hashgcdlem  12675  hashgcdeq  12677  pclem0  12724  pclemub  12725  pcprendvds2  12729  pcmul  12739  pcexp  12747  pcneg  12763  pc2dvds  12768  pcmpt  12781  prmpwdvds  12793  pockthg  12795  1arith  12805  4sqlem2  12827  4sqlemafi  12833  4sqlem11  12839  ennnfonelemex  12900  setscom  12987  subsubm  13430  insubm  13432  isgrpinv  13501  subsubg  13648  subsubrng  14091  subsubrg  14122  islss4  14259  znf1o  14528  znidomb  14535  tgcl  14651  lmbr2  14801  txcn  14862  txdis1cn  14865  txlm  14866  hmeoimaf1o  14901  txhmeo  14906  bl2in  14990  blssps  15014  blss  15015  blssexps  15016  blssex  15017  bdxmet  15088  xmetxp  15094  xmetxpbl  15095  xmettx  15097  metcnp3  15098  metcnpi3  15104  dedekindicc  15220  ivthdichlem  15238  limcimolemlt  15251  dvmptfsum  15312  rprelogbmul  15542  logbgcd1irr  15554  mpodvdsmulf1o  15577  lgsne0  15630  gausslemma2dlem1a  15650  lgseisenlem2  15663  lgsquadlemsfi  15667  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad2lem2  15674  2sqlem8  15715  2omap  16132  qdencn  16168  trilpolemlt1  16182