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  5135  f1oprg  5524  cnvf1olem  6250  tfrcl  6390  nnaordi  6534  swoer  6588  0er  6594  pw2f1odclem  6863  mapxpen  6877  fict  6897  dif1enen  6909  php5fin  6911  fin0  6914  fin0or  6915  diffisn  6922  infnfi  6924  unsnfi  6948  fidcenumlemrk  6984  sbthlemi8  6994  fiuni  7008  supmoti  7023  eldju2ndl  7102  eldju2ndr  7103  omp1eomlem  7124  difinfsnlem  7129  ctmlemr  7138  nninfwlpor  7203  exmidfodomrlemr  7232  exmidfodomrlemrALT  7233  enq0sym  7462  nqnq0pi  7468  addlocpr  7566  nqprl  7581  addnqprlemrl  7587  addnqprlemru  7588  mulnqprlemrl  7603  mulnqprlemru  7604  archpr  7673  cauappcvgprlemloc  7682  cauappcvgprlemladdfl  7685  archrecpr  7694  caucvgprlemdisj  7704  caucvgprlemloc  7705  caucvgprprlemml  7724  caucvgprprlemopl  7727  caucvgprprlemdisj  7732  caucvgprprlemloc  7733  suplocexprlemmu  7748  suplocexprlemdisj  7750  mulcmpblnrlemg  7770  caucvgsrlemgt1  7825  axarch  7921  axcaucvglemres  7929  cnegexlem2  8164  mulge0  8607  divdivap1  8711  divdivap2  8712  conjmulap  8717  ltdivmul  8864  nn0ge0div  9371  peano2uz2  9391  peano5uzti  9392  eluzp1m1  9583  xleadd1a  9905  iooshf  9984  divelunit  10034  eluzgtdifelfzo  10229  ioom  10293  modqcyc2  10393  modaddmodup  10420  uzennn  10469  seq3fveq2  10502  seq3id2  10542  seqfeq3  10545  expineg2  10563  mulexpzap  10594  leexp2r  10608  expnlbnd2  10680  hashfacen  10851  resqrexlemp1rp  11050  resqrexlemfp1  11053  negfi  11271  climcaucn  11394  fsum3cvg3  11439  fsum2dlemstep  11477  mptfzshft  11485  expcnvre  11546  fprodrev  11662  fprod2dlemstep  11665  moddvds  11841  dvdsflip  11892  addmodlteqALT  11900  nn0o  11947  zsupcllemex  11982  dfgcd2  12050  lcmgcdlem  12112  cncongr1  12138  prmind2  12155  isprm5lem  12176  isprm6  12182  cncongrprm  12192  oddpwdclemdc  12208  sqrt2irrap  12215  hashdvds  12256  crth  12259  prmdiveq  12271  hashgcdlem  12273  hashgcdeq  12274  pclem0  12321  pclemub  12322  pcprendvds2  12326  pcmul  12336  pcexp  12344  pcneg  12360  pc2dvds  12365  pcmpt  12378  prmpwdvds  12390  pockthg  12392  1arith  12402  4sqlem2  12424  4sqlemafi  12430  4sqlem11  12436  ennnfonelemex  12468  setscom  12555  subsubm  12950  insubm  12952  isgrpinv  13013  subsubg  13153  subsubrng  13578  subsubrg  13609  islss4  13715  tgcl  14041  lmbr2  14191  txcn  14252  txdis1cn  14255  txlm  14256  hmeoimaf1o  14291  txhmeo  14296  bl2in  14380  blssps  14404  blss  14405  blssexps  14406  blssex  14407  bdxmet  14478  xmetxp  14484  xmetxpbl  14485  xmettx  14487  metcnp3  14488  metcnpi3  14494  dedekindicc  14588  limcimolemlt  14610  rprelogbmul  14850  logbgcd1irr  14862  lgsne0  14917  lgseisenlem2  14929  2sqlem8  14948  qdencn  15254  trilpolemlt1  15268