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  6639  nnaordi  6785  swoer  6839  0er  6845  modom  7112  pw2f1odclem  7138  mapxpen  7152  mapunen  7155  fict  7174  dif1enen  7188  php5fin  7190  fin0  7193  fin0or  7194  diffisn  7201  infnfi  7203  unsnfi  7230  fidcenumlemrk  7276  sbthlemi8  7286  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  9744  peano2uz2  9764  peano5uzti  9765  eluzp1m1  9962  xleadd1a  10292  iooshf  10371  divelunit  10421  eluzgtdifelfzo  10632  zsupcllemex  10680  infssfzcldc  10686  infssfzledc  10687  ioom  10712  modqcyc2  10818  modaddmodup  10845  uzennn  10894  seq3fveq2  10933  seqfveq2g  10935  seq3id2  10984  seqfeq3  10987  expineg2  11006  mulexpzap  11037  leexp2r  11051  expnlbnd2  11124  hashmap  11290  sseqn  11301  hashfibclem  11304  hashfacen  11306  hashf1lem2  11308  hashf1  11309  wrdred1hash  11370  ccatsymb  11392  swrdwrdsymbg  11458  swrdsb0eq  11459  ccatpfx  11495  swrdswrd  11499  wrdind  11516  wrd2ind  11517  swrdccatin1  11519  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12  11527  pfxccat3  11528  swrdccat  11529  resqrexlemp1rp  11794  resqrexlemfp1  11797  negfi  12017  climcaucn  12142  fsum3cvg3  12188  fsum2dlemstep  12226  mptfzshft  12234  expcnvre  12295  fprodrev  12411  fprod2dlemstep  12414  moddvds  12591  dvdsflip  12643  addmodlteqALT  12651  nn0o  12699  dfgcd2  12816  lcmgcdlem  12880  cncongr1  12906  prmind2  12923  isprm5lem  12945  isprm6  12951  cncongrprm  12961  pwbdvdslemn  12969  nnmaxpw  12978  sqrt2irrap  12985  nn0sqdcq  13013  sqrtrirr  13014  hashdvds  13028  crth  13031  prmdiveq  13043  hashgcdlem  13045  hashgcdeq  13047  pclem0  13094  pclemub  13095  pcprendvds2  13099  pcmul  13109  pcexp  13117  pcneg  13133  pc2dvds  13138  pcmpt  13151  prmpwdvds  13163  pockthg  13165  1arith  13175  4sqlem2  13197  4sqlemafi  13203  4sqlem11  13209  ballotfilemsf1o  13315  ennnfonelemex  13363  setscom  13450  subsubm  13849  insubm  13851  isgrpinv  13918  subsubg  14059  gsum2d2fi  14274  subsubrng  14631  subsubrg  14662  islss4  14828  znf1o  15095  znidomb  15102  issubassa3  15121  tgcl  15290  lmbr2  15440  txcn  15501  txdis1cn  15504  txlm  15505  hmeoimaf1o  15540  txhmeo  15545  bl2in  15629  blssps  15653  blss  15654  blssexps  15655  blssex  15656  bdxmet  15727  xmetxp  15733  xmetxpbl  15734  xmettx  15736  metcnp3  15737  metcnpi3  15743  dedekindicc  15859  ivthdichlem  15877  limcimolemlt  15890  dvmptfsum  15951  rprelogbmul  16191  logbgcd1irr  16203  mpodvdsmulf1o  16284  lgsne0  16362  gausslemma2dlem1a  16382  lgseisenlem2  16395  lgsquadlemsfi  16399  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad2lem2  16406  2sqlem8  16447  uspgredg2vlem  16666  subuhgr  16718  subupgr  16719  subumgr  16720  iswlkg  16775  wlkl1loop  16804  upgriswlkdc  16806  clwwlkccatlem  16846  clwwlkn1loopb  16866  clwwlknonex2e  16886  qdencn  17278  trilpolemlt1  17297