Theorem ad2antll 482

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  521  simprrl  528  simprrr  529  dn1dc  944  prneimg  3701  f1oprg  5411  fvco4  5493  nnsucuniel  6391  mapen  6740  mapxpen  6742  fidceq  6763  fidifsnen  6764  php5fin  6776  findcard2d  6785  findcard2sd  6786  diffisn  6787  fidcenumlemr  6843  supmoti  6880  djuf1olem  6938  exmidfodomrlemim  7057  subhalfnqq  7222  nqnq0pi  7246  genprndl  7329  genprndu  7330  addlocpr  7344  nqprl  7359  nqpru  7360  addnqprlemrl  7365  addnqprlemru  7366  mullocpr  7379  mulnqprlemrl  7381  mulnqprlemru  7382  ltaprlem  7426  aptiprleml  7447  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  caucvgprlemladdfu  7485  caucvgprprlemloc  7511  suplocexprlemrl  7525  suplocexprlemru  7527  mulcmpblnrlemg  7548  recexgt0sr  7581  pitonn  7656  rereceu  7697  rimul  8347  receuap  8430  peano5uzti  9159  iooshf  9735  seq3fveq2  10242  seq3id2  10282  seqfeq3  10285  expcl2lemap  10305  mulexpzap  10333  expnlbnd2  10417  hashfacen  10579  absexpzap  10852  fsumf1o  11159  fisum0diag2  11216  fsummulc2  11217  moddvds  11502  dvdsflip  11549  dfgcd3  11698  dfgcd2  11702  lcmgcdlem  11758  cncongr1  11784  hashgcdlem  11903  setscom  11999  tgcl  12233  epttop  12259  cnpnei  12388  txcn  12444  txdis1cn  12447  imasnopn  12468  hmeoimaf1o  12483  txhmeo  12488  metss2lem  12666  bdxmet  12670  bdmopn  12673  metrest  12675  xmetxp  12676  metcnp  12681