Theorem ad2antrl 322

Description: Deduction adding conjuncts to an antecedent.

Hypothesis

Ref	Expression
ad2ant.1	⊢ (φ → ψ)

Assertion

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

Proof of Theorem ad2antrl

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

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  tz7.7 2224  onint 2261  tfrlem8 2956  tz7.48lem 2993  oalimcl 3162  sdomdomtr 3370  mapenlem2 3385  mapunen 3397  isfinite2 3437  aceq3 3556  aceq5 3563  axacnd 3758  ltapq 3870  ltexprlem7 3942  zltp1let 4597  peano2uz 4602  uzwo2 4606  uzwo3lem1 4614  infxpidmlem1 4933  ocsh 5164  projlem26 5218  pjpj0 5259  shmods 5363  osumlem7 5536  5oalem2 5545  3oalem2 5553  atom1d 5750  mdsymlem3 5778  mdsymlem5 5780  sumdmdi 5785  sumdmdlem 5786  sumdmd 5787

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