Theorem ad2antrl 494

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 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simprl  535  simprll  543  simprlr  544  elxp5  5279  f1oprg  5688  elovmporab1w  6293  cnvf1olem  6464  ressuppss  6498  tfrcl  6640  nnaordi  6786  swoer  6840  0er  6846  modom  7114  pw2f1odclem  7140  mapxpen  7154  mapunen  7157  fict  7176  dif1enen  7190  php5fin  7192  fin0  7195  fin0or  7196  diffisn  7203  infnfi  7205  unsnfi  7232  fidcenumlemrk  7278  sbthlemi8  7288  fiuni  7317  2omap  7324  supmoti  7339  eldju2ndl  7418  eldju2ndr  7419  omp1eomlem  7440  difinfsnlem  7445  ctmlemr  7454  nninfninc  7469  nninfwlpor  7520  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  enq0sym  7805  nqnq0pi  7811  addlocpr  7909  nqprl  7924  addnqprlemrl  7930  addnqprlemru  7931  mulnqprlemrl  7946  mulnqprlemru  7947  archpr  8016  cauappcvgprlemloc  8025  cauappcvgprlemladdfl  8028  archrecpr  8037  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprprlemml  8067  caucvgprprlemopl  8070  caucvgprprlemdisj  8075  caucvgprprlemloc  8076  suplocexprlemmu  8091  suplocexprlemdisj  8093  mulcmpblnrlemg  8113  caucvgsrlemgt1  8168  axarch  8264  axcaucvglemres  8272  cnegexlem2  8509  mulge0  8955  divdivap1  9061  divdivap2  9062  conjmulap  9067  ltdivmul  9214  nn0ge0div  9742  peano2uz2  9763  peano5uzti  9764  eluzp1m1  9961  xleadd1a  10291  iooshf  10370  divelunit  10420  eluzgtdifelfzo  10631  zsupcllemex  10679  infssfzcldc  10685  infssfzledc  10686  ioom  10711  modqcyc2  10817  modaddmodup  10844  uzennn  10893  seq3fveq2  10932  seqfveq2g  10934  seq3id2  10983  seqfeq3  10986  expineg2  11005  mulexpzap  11036  leexp2r  11050  expnlbnd2  11123  hashmap  11289  sseqn  11300  hashfibclem  11303  hashfacen  11305  hashf1lem2  11307  hashf1  11308  wrdred1hash  11369  ccatsymb  11391  swrdwrdsymbg  11457  swrdsb0eq  11458  ccatpfx  11494  swrdswrd  11498  wrdind  11515  wrd2ind  11516  swrdccatin1  11518  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12  11526  pfxccat3  11527  swrdccat  11528  resqrexlemp1rp  11793  resqrexlemfp1  11796  negfi  12016  climcaucn  12141  fsum3cvg3  12187  fsum2dlemstep  12225  mptfzshft  12233  expcnvre  12294  fprodrev  12410  fprod2dlemstep  12413  moddvds  12590  dvdsflip  12642  addmodlteqALT  12650  nn0o  12698  dfgcd2  12815  lcmgcdlem  12879  cncongr1  12905  prmind2  12922  isprm5lem  12944  isprm6  12950  cncongrprm  12960  pwbdvdslemn  12968  nnmaxpw  12977  sqrt2irrap  12984  nn0sqdcq  13012  sqrtrirr  13013  hashdvds  13027  crth  13030  prmdiveq  13042  hashgcdlem  13044  hashgcdeq  13046  pclem0  13093  pclemub  13094  pcprendvds2  13098  pcmul  13108  pcexp  13116  pcneg  13132  pc2dvds  13137  pcmpt  13150  prmpwdvds  13162  pockthg  13164  1arith  13174  4sqlem2  13196  4sqlemafi  13202  4sqlem11  13208  ballotfilemsf1o  13314  ennnfonelemex  13362  setscom  13449  subsubm  13848  insubm  13850  isgrpinv  13917  subsubg  14058  gsum2d2fi  14273  subsubrng  14630  subsubrg  14661  islss4  14827  znf1o  15094  znidomb  15101  issubassa3  15120  tgcl  15307  lmbr2  15457  txcn  15518  txdis1cn  15521  txlm  15522  hmeoimaf1o  15557  txhmeo  15562  bl2in  15646  blssps  15670  blss  15671  blssexps  15672  blssex  15673  bdxmet  15744  xmetxp  15750  xmetxpbl  15751  xmettx  15753  metcnp3  15754  metcnpi3  15760  dedekindicc  15876  ivthdichlem  15894  limcimolemlt  15907  dvmptfsum  15968  rprelogbmul  16208  logbgcd1irr  16220  mpodvdsmulf1o  16301  lgsne0  16379  gausslemma2dlem1a  16399  lgseisenlem2  16412  lgsquadlemsfi  16416  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad2lem2  16423  2sqlem8  16464  uspgredg2vlem  16683  subuhgr  16735  subupgr  16736  subumgr  16737  iswlkg  16792  wlkl1loop  16821  upgriswlkdc  16823  clwwlkccatlem  16863  clwwlkn1loopb  16883  clwwlknonex2e  16903  qdencn  17295  trilpolemlt1  17314