Theorem ad2antrl 475

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 271	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantl 272	1 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simprl  499  simprll  505  simprlr  506  elxp5  4953  f1oprg  5330  cnvf1olem  6027  tfrcl  6167  nnaordi  6307  swoer  6360  0er  6366  mapxpen  6644  fict  6664  dif1enen  6676  php5fin  6678  fin0  6681  fin0or  6682  diffisn  6689  infnfi  6691  unsnfi  6709  fidcenumlemrk  6743  sbthlemi8  6753  supmoti  6768  eldju2ndl  6843  eldju2ndr  6844  ctmlemr  6870  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  enq0sym  7088  nqnq0pi  7094  addlocpr  7192  nqprl  7207  addnqprlemrl  7213  addnqprlemru  7214  mulnqprlemrl  7229  mulnqprlemru  7230  archpr  7299  cauappcvgprlemloc  7308  cauappcvgprlemladdfl  7311  archrecpr  7320  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprprlemml  7350  caucvgprprlemopl  7353  caucvgprprlemdisj  7358  caucvgprprlemloc  7359  mulcmpblnrlemg  7383  caucvgsrlemgt1  7437  axarch  7523  axcaucvglemres  7531  cnegexlem2  7755  mulge0  8193  divdivap1  8287  divdivap2  8288  conjmulap  8293  ltdivmul  8434  nn0ge0div  8932  peano2uz2  8952  peano5uzti  8953  eluzp1m1  9141  xleadd1a  9439  iooshf  9518  divelunit  9568  eluzgtdifelfzo  9757  ioom  9821  modqcyc2  9916  modaddmodup  9943  iseqval  10017  seq3fveq2  10034  seq3id2  10075  seqfeq3  10078  expineg2  10095  mulexpzap  10126  leexp2r  10140  expnlbnd2  10210  hashfacen  10372  resqrexlemp1rp  10570  resqrexlemfp1  10573  negfi  10790  climcaucn  10910  fsum3cvg3  10955  fsum2dlemstep  10993  mptfzshft  11001  expcnvre  11062  moddvds  11248  dvdsflip  11295  addmodlteqALT  11303  nn0o  11350  zsupcllemex  11385  dfgcd2  11446  lcmgcdlem  11502  cncongr1  11528  prmind2  11545  isprm6  11569  cncongrprm  11579  oddpwdclemdc  11594  sqrt2irrap  11601  hashdvds  11640  crth  11643  hashgcdlem  11646  hashgcdeq  11647  setscom  11699  tgcl  11932  lmbr2  12081  bl2in  12205  blssps  12229  blss  12230  blssexps  12231  blssex  12232  bdxmet  12303  metcnp3  12309  metcnpi3  12315  qdencn  12636