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  5159  f1oprg  5549  elovmporab1w  6126  cnvf1olem  6284  tfrcl  6424  nnaordi  6568  swoer  6622  0er  6628  pw2f1odclem  6897  mapxpen  6911  fict  6931  dif1enen  6943  php5fin  6945  fin0  6948  fin0or  6949  diffisn  6956  infnfi  6958  unsnfi  6982  fidcenumlemrk  7022  sbthlemi8  7032  fiuni  7046  supmoti  7061  eldju2ndl  7140  eldju2ndr  7141  omp1eomlem  7162  difinfsnlem  7167  ctmlemr  7176  nninfninc  7191  nninfwlpor  7242  exmidfodomrlemr  7272  exmidfodomrlemrALT  7273  enq0sym  7502  nqnq0pi  7508  addlocpr  7606  nqprl  7621  addnqprlemrl  7627  addnqprlemru  7628  mulnqprlemrl  7643  mulnqprlemru  7644  archpr  7713  cauappcvgprlemloc  7722  cauappcvgprlemladdfl  7725  archrecpr  7734  caucvgprlemdisj  7744  caucvgprlemloc  7745  caucvgprprlemml  7764  caucvgprprlemopl  7767  caucvgprprlemdisj  7772  caucvgprprlemloc  7773  suplocexprlemmu  7788  suplocexprlemdisj  7790  mulcmpblnrlemg  7810  caucvgsrlemgt1  7865  axarch  7961  axcaucvglemres  7969  cnegexlem2  8205  mulge0  8649  divdivap1  8753  divdivap2  8754  conjmulap  8759  ltdivmul  8906  nn0ge0div  9416  peano2uz2  9436  peano5uzti  9437  eluzp1m1  9628  xleadd1a  9951  iooshf  10030  divelunit  10080  eluzgtdifelfzo  10276  zsupcllemex  10323  ioom  10353  modqcyc2  10455  modaddmodup  10482  uzennn  10531  seq3fveq2  10570  seqfveq2g  10572  seq3id2  10621  seqfeq3  10624  expineg2  10643  mulexpzap  10674  leexp2r  10688  expnlbnd2  10760  hashfacen  10931  wrdred1hash  10981  resqrexlemp1rp  11174  resqrexlemfp1  11177  negfi  11396  climcaucn  11519  fsum3cvg3  11564  fsum2dlemstep  11602  mptfzshft  11610  expcnvre  11671  fprodrev  11787  fprod2dlemstep  11790  moddvds  11967  dvdsflip  12019  addmodlteqALT  12027  nn0o  12075  dfgcd2  12192  lcmgcdlem  12256  cncongr1  12282  prmind2  12299  isprm5lem  12320  isprm6  12326  cncongrprm  12336  oddpwdclemdc  12352  sqrt2irrap  12359  hashdvds  12400  crth  12403  prmdiveq  12415  hashgcdlem  12417  hashgcdeq  12419  pclem0  12466  pclemub  12467  pcprendvds2  12471  pcmul  12481  pcexp  12489  pcneg  12505  pc2dvds  12510  pcmpt  12523  prmpwdvds  12535  pockthg  12537  1arith  12547  4sqlem2  12569  4sqlemafi  12575  4sqlem11  12581  ennnfonelemex  12642  setscom  12729  subsubm  13141  insubm  13143  isgrpinv  13212  subsubg  13353  subsubrng  13796  subsubrg  13827  islss4  13964  znf1o  14233  znidomb  14240  tgcl  14326  lmbr2  14476  txcn  14537  txdis1cn  14540  txlm  14541  hmeoimaf1o  14576  txhmeo  14581  bl2in  14665  blssps  14689  blss  14690  blssexps  14691  blssex  14692  bdxmet  14763  xmetxp  14769  xmetxpbl  14770  xmettx  14772  metcnp3  14773  metcnpi3  14779  dedekindicc  14895  ivthdichlem  14913  limcimolemlt  14926  dvmptfsum  14987  rprelogbmul  15217  logbgcd1irr  15229  mpodvdsmulf1o  15252  lgsne0  15305  gausslemma2dlem1a  15325  lgseisenlem2  15338  lgsquadlemsfi  15342  lgsquadlem1  15344  lgsquadlem2  15345  lgsquadlem3  15346  lgsquad2lem2  15349  2sqlem8  15390  2omap  15668  qdencn  15700  trilpolemlt1  15714