Theorem ad2antrl 474

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  simprl  498  simprll  504  simprlr  505  elxp5  4885  f1oprg  5258  cnvf1olem  5946  tfrcl  6083  nnaordi  6219  swoer  6272  0er  6278  mapxpen  6516  fict  6536  dif1enen  6548  php5fin  6550  fin0  6553  fin0or  6554  diffisn  6561  infnfi  6563  unsnfi  6581  sbthlemi8  6617  supmoti  6632  eldju2ndl  6707  eldju2ndr  6708  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  enq0sym  6935  nqnq0pi  6941  addlocpr  7039  nqprl  7054  addnqprlemrl  7060  addnqprlemru  7061  mulnqprlemrl  7076  mulnqprlemru  7077  archpr  7146  cauappcvgprlemloc  7155  cauappcvgprlemladdfl  7158  archrecpr  7167  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprprlemml  7197  caucvgprprlemopl  7200  caucvgprprlemdisj  7205  caucvgprprlemloc  7206  mulcmpblnrlemg  7230  caucvgsrlemgt1  7284  axarch  7370  axcaucvglemres  7378  cnegexlem2  7602  mulge0  8037  divdivap1  8129  divdivap2  8130  conjmulap  8135  ltdivmul  8272  nn0ge0div  8766  peano2uz2  8786  peano5uzti  8787  eluzp1m1  8974  iooshf  9302  divelunit  9351  eluzgtdifelfzo  9536  ioom  9600  modqcyc2  9695  modaddmodup  9722  iseqval  9788  iseqfveq2  9802  iseqid2  9843  expineg2  9862  mulexpzap  9893  leexp2r  9907  expnlbnd2  9975  hashfacen  10137  resqrexlemp1rp  10334  resqrexlemfp1  10337  negfi  10552  climcaucn  10630  moddvds  10680  dvdsflip  10727  addmodlteqALT  10735  nn0o  10782  zsupcllemex  10817  dfgcd2  10878  lcmgcdlem  10934  cncongr1  10960  prmind2  10977  isprm6  11001  cncongrprm  11011  oddpwdclemdc  11026  sqrt2irrap  11033  hashdvds  11072  crth  11075  hashgcdlem  11078  hashgcdeq  11079  qdencn  11353