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  531  simprll  539  simprlr  540  elxp5  5225  f1oprg  5629  elovmporab1w  6222  cnvf1olem  6388  tfrcl  6529  nnaordi  6675  swoer  6729  0er  6735  modom  6993  pw2f1odclem  7019  mapxpen  7033  fict  7054  dif1enen  7068  php5fin  7070  fin0  7073  fin0or  7074  diffisn  7081  infnfi  7083  unsnfi  7110  fidcenumlemrk  7152  sbthlemi8  7162  fiuni  7176  supmoti  7191  eldju2ndl  7270  eldju2ndr  7271  omp1eomlem  7292  difinfsnlem  7297  ctmlemr  7306  nninfninc  7321  nninfwlpor  7372  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  enq0sym  7651  nqnq0pi  7657  addlocpr  7755  nqprl  7770  addnqprlemrl  7776  addnqprlemru  7777  mulnqprlemrl  7792  mulnqprlemru  7793  archpr  7862  cauappcvgprlemloc  7871  cauappcvgprlemladdfl  7874  archrecpr  7883  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprprlemml  7913  caucvgprprlemopl  7916  caucvgprprlemdisj  7921  caucvgprprlemloc  7922  suplocexprlemmu  7937  suplocexprlemdisj  7939  mulcmpblnrlemg  7959  caucvgsrlemgt1  8014  axarch  8110  axcaucvglemres  8118  cnegexlem2  8354  mulge0  8798  divdivap1  8902  divdivap2  8903  conjmulap  8908  ltdivmul  9055  nn0ge0div  9566  peano2uz2  9586  peano5uzti  9587  eluzp1m1  9779  xleadd1a  10107  iooshf  10186  divelunit  10236  eluzgtdifelfzo  10441  zsupcllemex  10489  ioom  10519  modqcyc2  10621  modaddmodup  10648  uzennn  10697  seq3fveq2  10736  seqfveq2g  10738  seq3id2  10787  seqfeq3  10790  expineg2  10809  mulexpzap  10840  leexp2r  10854  expnlbnd2  10926  hashfacen  11099  wrdred1hash  11156  ccatsymb  11178  swrdwrdsymbg  11244  swrdsb0eq  11245  ccatpfx  11281  swrdswrd  11285  wrdind  11302  wrd2ind  11303  swrdccatin1  11305  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12  11313  pfxccat3  11314  swrdccat  11315  resqrexlemp1rp  11566  resqrexlemfp1  11569  negfi  11788  climcaucn  11911  fsum3cvg3  11956  fsum2dlemstep  11994  mptfzshft  12002  expcnvre  12063  fprodrev  12179  fprod2dlemstep  12182  moddvds  12359  dvdsflip  12411  addmodlteqALT  12419  nn0o  12467  dfgcd2  12584  lcmgcdlem  12648  cncongr1  12674  prmind2  12691  isprm5lem  12712  isprm6  12718  cncongrprm  12728  oddpwdclemdc  12744  sqrt2irrap  12751  hashdvds  12792  crth  12795  prmdiveq  12807  hashgcdlem  12809  hashgcdeq  12811  pclem0  12858  pclemub  12859  pcprendvds2  12863  pcmul  12873  pcexp  12881  pcneg  12897  pc2dvds  12902  pcmpt  12915  prmpwdvds  12927  pockthg  12929  1arith  12939  4sqlem2  12961  4sqlemafi  12967  4sqlem11  12973  ennnfonelemex  13034  setscom  13121  subsubm  13565  insubm  13567  isgrpinv  13636  subsubg  13783  subsubrng  14227  subsubrg  14258  islss4  14395  znf1o  14664  znidomb  14671  tgcl  14787  lmbr2  14937  txcn  14998  txdis1cn  15001  txlm  15002  hmeoimaf1o  15037  txhmeo  15042  bl2in  15126  blssps  15150  blss  15151  blssexps  15152  blssex  15153  bdxmet  15224  xmetxp  15230  xmetxpbl  15231  xmettx  15233  metcnp3  15234  metcnpi3  15240  dedekindicc  15356  ivthdichlem  15374  limcimolemlt  15387  dvmptfsum  15448  rprelogbmul  15678  logbgcd1irr  15690  mpodvdsmulf1o  15713  lgsne0  15766  gausslemma2dlem1a  15786  lgseisenlem2  15799  lgsquadlemsfi  15803  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem2  15810  2sqlem8  15851  uspgredg2vlem  16070  subuhgr  16122  subupgr  16123  subumgr  16124  iswlkg  16179  wlkl1loop  16208  upgriswlkdc  16210  clwwlkccatlem  16250  clwwlkn1loopb  16270  clwwlknonex2e  16290  2omap  16594  qdencn  16631  trilpolemlt1  16645