Theorem ad2antrr 323

Description: Deduction adding conjuncts to an antecedent.

Hypothesis

Ref	Expression
ad2ant.1	⊢ (φ → ψ)

Assertion

Ref	Expression
ad2antrr	⊢ ((χ ∧ (θ ∧ φ)) → ψ)

Proof of Theorem ad2antrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (φ → ψ)
2	1	adantl 305	. 2 ⊢ ((θ ∧ φ) → ψ)
3	2	adantl 305	1 ⊢ ((χ ∧ (θ ∧ φ)) → ψ)

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  ordsucelsuc 2324  funfvima3 2906  isomin 2937  oalimcl 3162  pw2en 3348  axacndlem5 3757  axacnd 3758  uzwo 4605  nnwoOLD 4608  replimt 4798  chocuni 5179  spansneleq 5475  osumlem7 5536  3oalem2 5553  stles 5682  atss 5744

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org