Theorem ad2antll 483

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 275	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜓)
3	2	adantl 275	1 ⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simprr  522  simprrl  529  simprrr  530  dn1dc  950  prneimg  3754  f1oprg  5476  fvco4  5558  nnsucuniel  6463  mapen  6812  mapxpen  6814  fidceq  6835  fidifsnen  6836  php5fin  6848  findcard2d  6857  findcard2sd  6858  diffisn  6859  fidcenumlemr  6920  supmoti  6958  djuf1olem  7018  exmidfodomrlemim  7157  cc4f  7210  cc4n  7212  subhalfnqq  7355  nqnq0pi  7379  genprndl  7462  genprndu  7463  addlocpr  7477  nqprl  7492  nqpru  7493  addnqprlemrl  7498  addnqprlemru  7499  mullocpr  7512  mulnqprlemrl  7514  mulnqprlemru  7515  ltaprlem  7559  aptiprleml  7580  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  caucvgprlemladdfu  7618  caucvgprprlemloc  7644  suplocexprlemrl  7658  suplocexprlemru  7660  mulcmpblnrlemg  7681  recexgt0sr  7714  pitonn  7789  rereceu  7830  rimul  8483  receuap  8566  peano5uzti  9299  iooshf  9888  seq3fveq2  10404  seq3id2  10444  seqfeq3  10447  expcl2lemap  10467  mulexpzap  10495  expnlbnd2  10580  hashfacen  10749  absexpzap  11022  fsumf1o  11331  fisum0diag2  11388  fsummulc2  11389  fprodmul  11532  fprodrev  11560  moddvds  11739  dvdsflip  11789  dfgcd3  11943  dfgcd2  11947  lcmgcdlem  12009  cncongr1  12035  hashgcdlem  12170  phisum  12172  pcval  12228  pcqcl  12238  pcid  12255  pcneg  12256  prmpwdvds  12285  pockthg  12287  4sqlem2  12319  setscom  12434  tgcl  12704  epttop  12730  cnpnei  12859  txcn  12915  txdis1cn  12918  imasnopn  12939  hmeoimaf1o  12954  txhmeo  12959  metss2lem  13137  bdxmet  13141  bdmopn  13144  metrest  13146  xmetxp  13147  metcnp  13152  rprelogbmul  13513  logbgcd1irr  13525