Theorem ad2antll 495

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

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:  simprr  537  simprrl  545  simprrr  546  dn1dc  973  prneimg  3899  f1oprg  5685  fvco4  5777  nnsucuniel  6768  modom  7108  mapen  7146  mapxpen  7148  mapunen  7151  fidceq  7171  fidifsnen  7172  php5fin  7186  findcard2d  7195  findcard2sd  7196  diffisn  7197  fidcenumlemr  7272  supmoti  7334  djuf1olem  7394  nninfwlpor  7515  exmidfodomrlemim  7554  cc4f  7636  cc4n  7638  subhalfnqq  7782  nqnq0pi  7806  genprndl  7889  genprndu  7890  addlocpr  7904  nqprl  7919  nqpru  7920  addnqprlemrl  7925  addnqprlemru  7926  mullocpr  7939  mulnqprlemrl  7941  mulnqprlemru  7942  ltaprlem  7986  aptiprleml  8007  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  caucvgprlemladdfu  8045  caucvgprprlemloc  8071  suplocexprlemrl  8085  suplocexprlemru  8087  mulcmpblnrlemg  8108  recexgt0sr  8141  pitonn  8216  rereceu  8257  rimul  8916  receuap  9002  peano5uzti  9759  iooshf  10365  seq3fveq2  10927  seqfveq2g  10929  seq3id2  10978  seqfeq3  10981  expcl2lemap  11003  mulexpzap  11031  expnlbnd2  11118  hashfacen  11300  hashf1lem1  11301  fstwrdne0  11360  swrdsb0eq  11453  swrdswrd  11493  wrd2ind  11511  swrdccatin1  11513  pfxccatin12  11521  pfxccat3  11522  swrdccat  11523  absexpzap  11863  fsumf1o  12176  fisum0diag2  12233  fsummulc2  12234  fprodmul  12377  fprodrev  12405  moddvds  12585  dvdsflip  12637  dfgcd3  12806  dfgcd2  12810  lcmgcdlem  12874  cncongr1  12900  hashgcdlem  13039  phisum  13042  pcval  13098  pcqcl  13108  pcid  13126  pcneg  13127  prmpwdvds  13157  pockthg  13159  4sqlem2  13191  4sqlem11  13203  ballotfilemsf1o  13309  setscom  13444  qusval  13697  mulgdirlem  14009  mulgass  14015  0nsg  14070  ghmmulg  14112  islmodd  14713  lmodvsmmulgdi  14744  islss3  14800  znf1o  15070  tgcl  15256  epttop  15282  cnpnei  15411  txcn  15467  txdis1cn  15470  imasnopn  15491  hmeoimaf1o  15506  txhmeo  15511  metss2lem  15689  bdxmet  15693  bdmopn  15696  metrest  15698  xmetxp  15699  metcnp  15704  dvmptfsum  15917  plycn  15954  dvply2g  15958  rprelogbmul  16152  logbgcd1irr  16164  mpodvdsmulf1o  16245  chtublem  16256  gausslemma2dlem1a  16343  lgseisenlem2  16356  lgsquadlemsfi  16360  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  subgrprop3  16669  subupgr  16680  wlkl1loop  16765  clwwlknp  16824