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  7318  supmoti  7333  eldju2ndl  7412  eldju2ndr  7413  omp1eomlem  7434  difinfsnlem  7439  ctmlemr  7448  nninfninc  7463  nninfwlpor  7514  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  enq0sym  7799  nqnq0pi  7805  addlocpr  7903  nqprl  7918  addnqprlemrl  7924  addnqprlemru  7925  mulnqprlemrl  7940  mulnqprlemru  7941  archpr  8010  cauappcvgprlemloc  8019  cauappcvgprlemladdfl  8022  archrecpr  8031  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprprlemml  8061  caucvgprprlemopl  8064  caucvgprprlemdisj  8069  caucvgprprlemloc  8070  suplocexprlemmu  8085  suplocexprlemdisj  8087  mulcmpblnrlemg  8107  caucvgsrlemgt1  8162  axarch  8258  axcaucvglemres  8266  cnegexlem2  8502  mulge0  8947  divdivap1  9053  divdivap2  9054  conjmulap  9059  ltdivmul  9206  nn0ge0div  9733  peano2uz2  9753  peano5uzti  9754  eluzp1m1  9946  xleadd1a  10275  iooshf  10354  divelunit  10404  eluzgtdifelfzo  10615  zsupcllemex  10663  infssfzcldc  10669  infssfzledc  10670  ioom  10695  modqcyc2  10797  modaddmodup  10824  uzennn  10873  seq3fveq2  10912  seqfveq2g  10914  seq3id2  10963  seqfeq3  10966  expineg2  10985  mulexpzap  11016  leexp2r  11030  expnlbnd2  11103  hashmap  11268  sseqn  11279  hashfibclem  11282  hashfacen  11284  hashf1lem2  11286  hashf1  11287  wrdred1hash  11348  ccatsymb  11370  swrdwrdsymbg  11436  swrdsb0eq  11437  ccatpfx  11473  swrdswrd  11477  wrdind  11494  wrd2ind  11495  swrdccatin1  11497  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12  11505  pfxccat3  11506  swrdccat  11507  resqrexlemp1rp  11772  resqrexlemfp1  11775  negfi  11994  climcaucn  12117  fsum3cvg3  12163  fsum2dlemstep  12201  mptfzshft  12209  expcnvre  12270  fprodrev  12386  fprod2dlemstep  12389  moddvds  12566  dvdsflip  12618  addmodlteqALT  12626  nn0o  12674  dfgcd2  12791  lcmgcdlem  12855  cncongr1  12881  prmind2  12898  isprm5lem  12919  isprm6  12925  cncongrprm  12935  oddpwdclemdc  12951  sqrt2irrap  12958  hashdvds  12999  crth  13002  prmdiveq  13014  hashgcdlem  13016  hashgcdeq  13018  pclem0  13065  pclemub  13066  pcprendvds2  13070  pcmul  13080  pcexp  13088  pcneg  13104  pc2dvds  13109  pcmpt  13122  prmpwdvds  13134  pockthg  13136  1arith  13146  4sqlem2  13168  4sqlemafi  13174  4sqlem11  13180  ballotfilemsf1o  13257  ennnfonelemex  13305  setscom  13392  subsubm  13790  insubm  13792  isgrpinv  13859  subsubg  14000  subsubrng  14522  subsubrg  14553  islss4  14719  znf1o  14986  znidomb  14993  issubassa3  15012  tgcl  15165  lmbr2  15315  txcn  15376  txdis1cn  15379  txlm  15380  hmeoimaf1o  15415  txhmeo  15420  bl2in  15504  blssps  15528  blss  15529  blssexps  15530  blssex  15531  bdxmet  15602  xmetxp  15608  xmetxpbl  15609  xmettx  15611  metcnp3  15612  metcnpi3  15618  dedekindicc  15734  ivthdichlem  15752  limcimolemlt  15765  dvmptfsum  15826  rprelogbmul  16057  logbgcd1irr  16069  mpodvdsmulf1o  16104  lgsne0  16157  gausslemma2dlem1a  16177  lgseisenlem2  16190  lgsquadlemsfi  16194  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem2  16201  2sqlem8  16242  uspgredg2vlem  16461  subuhgr  16513  subupgr  16514  subumgr  16515  iswlkg  16570  wlkl1loop  16599  upgriswlkdc  16601  clwwlkccatlem  16641  clwwlkn1loopb  16661  clwwlknonex2e  16681  qdencn  17072  trilpolemlt1  17090