Theorem ad2antrl 494

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 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simprl  535  simprll  543  simprlr  544  elxp5  5276  f1oprg  5685  elovmporab1w  6290  cnvf1olem  6460  ressuppss  6494  tfrcl  6635  nnaordi  6781  swoer  6835  0er  6841  modom  7108  pw2f1odclem  7134  mapxpen  7148  mapunen  7151  fict  7170  dif1enen  7184  php5fin  7186  fin0  7189  fin0or  7190  diffisn  7197  infnfi  7199  unsnfi  7226  fidcenumlemrk  7271  sbthlemi8  7281  fiuni  7312  2omap  7319  supmoti  7334  eldju2ndl  7413  eldju2ndr  7414  omp1eomlem  7435  difinfsnlem  7440  ctmlemr  7449  nninfninc  7464  nninfwlpor  7515  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  enq0sym  7800  nqnq0pi  7806  addlocpr  7904  nqprl  7919  addnqprlemrl  7925  addnqprlemru  7926  mulnqprlemrl  7941  mulnqprlemru  7942  archpr  8011  cauappcvgprlemloc  8020  cauappcvgprlemladdfl  8023  archrecpr  8032  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprprlemml  8062  caucvgprprlemopl  8065  caucvgprprlemdisj  8070  caucvgprprlemloc  8071  suplocexprlemmu  8086  suplocexprlemdisj  8088  mulcmpblnrlemg  8108  caucvgsrlemgt1  8163  axarch  8259  axcaucvglemres  8267  cnegexlem2  8504  mulge0  8950  divdivap1  9056  divdivap2  9057  conjmulap  9062  ltdivmul  9209  nn0ge0div  9738  peano2uz2  9758  peano5uzti  9759  eluzp1m1  9956  xleadd1a  10286  iooshf  10365  divelunit  10415  eluzgtdifelfzo  10626  zsupcllemex  10674  infssfzcldc  10680  infssfzledc  10681  ioom  10706  modqcyc2  10812  modaddmodup  10839  uzennn  10888  seq3fveq2  10927  seqfveq2g  10929  seq3id2  10978  seqfeq3  10981  expineg2  11000  mulexpzap  11031  leexp2r  11045  expnlbnd2  11118  hashmap  11284  sseqn  11295  hashfibclem  11298  hashfacen  11300  hashf1lem2  11302  hashf1  11303  wrdred1hash  11364  ccatsymb  11386  swrdwrdsymbg  11452  swrdsb0eq  11453  ccatpfx  11489  swrdswrd  11493  wrdind  11510  wrd2ind  11511  swrdccatin1  11513  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12  11521  pfxccat3  11522  swrdccat  11523  resqrexlemp1rp  11788  resqrexlemfp1  11791  negfi  12011  climcaucn  12136  fsum3cvg3  12182  fsum2dlemstep  12220  mptfzshft  12228  expcnvre  12289  fprodrev  12405  fprod2dlemstep  12408  moddvds  12585  dvdsflip  12637  addmodlteqALT  12645  nn0o  12693  dfgcd2  12810  lcmgcdlem  12874  cncongr1  12900  prmind2  12917  isprm5lem  12939  isprm6  12945  cncongrprm  12955  pwbdvdslemn  12963  nnmaxpw  12972  sqrt2irrap  12979  nn0sqdcq  13007  sqrtrirr  13008  hashdvds  13022  crth  13025  prmdiveq  13037  hashgcdlem  13039  hashgcdeq  13041  pclem0  13088  pclemub  13089  pcprendvds2  13093  pcmul  13103  pcexp  13111  pcneg  13127  pc2dvds  13132  pcmpt  13145  prmpwdvds  13157  pockthg  13159  1arith  13169  4sqlem2  13191  4sqlemafi  13197  4sqlem11  13203  ballotfilemsf1o  13309  ennnfonelemex  13357  setscom  13444  subsubm  13843  insubm  13845  isgrpinv  13912  subsubg  14053  subsubrng  14606  subsubrg  14637  islss4  14803  znf1o  15070  znidomb  15077  issubassa3  15096  tgcl  15256  lmbr2  15406  txcn  15467  txdis1cn  15470  txlm  15471  hmeoimaf1o  15506  txhmeo  15511  bl2in  15595  blssps  15619  blss  15620  blssexps  15621  blssex  15622  bdxmet  15693  xmetxp  15699  xmetxpbl  15700  xmettx  15702  metcnp3  15703  metcnpi3  15709  dedekindicc  15825  ivthdichlem  15843  limcimolemlt  15856  dvmptfsum  15917  rprelogbmul  16152  logbgcd1irr  16164  mpodvdsmulf1o  16245  lgsne0  16323  gausslemma2dlem1a  16343  lgseisenlem2  16356  lgsquadlemsfi  16360  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad2lem2  16367  2sqlem8  16408  uspgredg2vlem  16627  subuhgr  16679  subupgr  16680  subumgr  16681  iswlkg  16736  wlkl1loop  16765  upgriswlkdc  16767  clwwlkccatlem  16807  clwwlkn1loopb  16827  clwwlknonex2e  16847  qdencn  17238  trilpolemlt1  17257