Theorem ad2antll 491

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad2antll	⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)

Proof of Theorem ad2antll

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 277	. 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:  simprr  533  simprrl  541  simprrr  542  dn1dc  968  prneimg  3857  f1oprg  5629  fvco4  5718  nnsucuniel  6663  modom  6994  mapen  7032  mapxpen  7034  fidceq  7056  fidifsnen  7057  php5fin  7071  findcard2d  7080  findcard2sd  7081  diffisn  7082  fidcenumlemr  7154  supmoti  7192  djuf1olem  7252  nninfwlpor  7373  exmidfodomrlemim  7412  cc4f  7488  cc4n  7490  subhalfnqq  7634  nqnq0pi  7658  genprndl  7741  genprndu  7742  addlocpr  7756  nqprl  7771  nqpru  7772  addnqprlemrl  7777  addnqprlemru  7778  mullocpr  7791  mulnqprlemrl  7793  mulnqprlemru  7794  ltaprlem  7838  aptiprleml  7859  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  caucvgprlemladdfu  7897  caucvgprprlemloc  7923  suplocexprlemrl  7937  suplocexprlemru  7939  mulcmpblnrlemg  7960  recexgt0sr  7993  pitonn  8068  rereceu  8109  rimul  8765  receuap  8849  peano5uzti  9588  iooshf  10187  seq3fveq2  10738  seqfveq2g  10740  seq3id2  10789  seqfeq3  10792  expcl2lemap  10814  mulexpzap  10842  expnlbnd2  10928  hashfacen  11101  fstwrdne0  11157  swrdsb0eq  11250  swrdswrd  11290  wrd2ind  11308  swrdccatin1  11310  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  absexpzap  11658  fsumf1o  11969  fisum0diag2  12026  fsummulc2  12027  fprodmul  12170  fprodrev  12198  moddvds  12378  dvdsflip  12430  dfgcd3  12599  dfgcd2  12603  lcmgcdlem  12667  cncongr1  12693  hashgcdlem  12828  phisum  12831  pcval  12887  pcqcl  12897  pcid  12915  pcneg  12916  prmpwdvds  12946  pockthg  12948  4sqlem2  12980  4sqlem11  12992  setscom  13140  qusval  13424  mulgdirlem  13758  mulgass  13764  0nsg  13819  ghmmulg  13861  islmodd  14326  lmodvsmmulgdi  14356  islss3  14412  znf1o  14684  tgcl  14807  epttop  14833  cnpnei  14962  txcn  15018  txdis1cn  15021  imasnopn  15042  hmeoimaf1o  15057  txhmeo  15062  metss2lem  15240  bdxmet  15244  bdmopn  15247  metrest  15249  xmetxp  15250  metcnp  15255  dvmptfsum  15468  plycn  15505  dvply2g  15509  rprelogbmul  15698  logbgcd1irr  15710  mpodvdsmulf1o  15733  gausslemma2dlem1a  15806  lgseisenlem2  15819  lgsquadlemsfi  15823  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  subgrprop3  16132  subupgr  16143  wlkl1loop  16228  clwwlknp  16287