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  6662  modom  6993  mapen  7031  mapxpen  7033  fidceq  7055  fidifsnen  7056  php5fin  7070  findcard2d  7079  findcard2sd  7080  diffisn  7081  fidcenumlemr  7153  supmoti  7191  djuf1olem  7251  nninfwlpor  7372  exmidfodomrlemim  7411  cc4f  7487  cc4n  7489  subhalfnqq  7633  nqnq0pi  7657  genprndl  7740  genprndu  7741  addlocpr  7755  nqprl  7770  nqpru  7771  addnqprlemrl  7776  addnqprlemru  7777  mullocpr  7790  mulnqprlemrl  7792  mulnqprlemru  7793  ltaprlem  7837  aptiprleml  7858  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  caucvgprlemladdfu  7896  caucvgprprlemloc  7922  suplocexprlemrl  7936  suplocexprlemru  7938  mulcmpblnrlemg  7959  recexgt0sr  7992  pitonn  8067  rereceu  8108  rimul  8764  receuap  8848  peano5uzti  9587  iooshf  10186  seq3fveq2  10736  seqfveq2g  10738  seq3id2  10787  seqfeq3  10790  expcl2lemap  10812  mulexpzap  10840  expnlbnd2  10926  hashfacen  11099  fstwrdne0  11152  swrdsb0eq  11245  swrdswrd  11285  wrd2ind  11303  swrdccatin1  11305  pfxccatin12  11313  pfxccat3  11314  swrdccat  11315  absexpzap  11640  fsumf1o  11950  fisum0diag2  12007  fsummulc2  12008  fprodmul  12151  fprodrev  12179  moddvds  12359  dvdsflip  12411  dfgcd3  12580  dfgcd2  12584  lcmgcdlem  12648  cncongr1  12674  hashgcdlem  12809  phisum  12812  pcval  12868  pcqcl  12878  pcid  12896  pcneg  12897  prmpwdvds  12927  pockthg  12929  4sqlem2  12961  4sqlem11  12973  setscom  13121  qusval  13405  mulgdirlem  13739  mulgass  13745  0nsg  13800  ghmmulg  13842  islmodd  14306  lmodvsmmulgdi  14336  islss3  14392  znf1o  14664  tgcl  14787  epttop  14813  cnpnei  14942  txcn  14998  txdis1cn  15001  imasnopn  15022  hmeoimaf1o  15037  txhmeo  15042  metss2lem  15220  bdxmet  15224  bdmopn  15227  metrest  15229  xmetxp  15230  metcnp  15235  dvmptfsum  15448  plycn  15485  dvply2g  15489  rprelogbmul  15678  logbgcd1irr  15690  mpodvdsmulf1o  15713  gausslemma2dlem1a  15786  lgseisenlem2  15799  lgsquadlemsfi  15803  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  subgrprop3  16112  subupgr  16123  wlkl1loop  16208  clwwlknp  16267