Theorem ad2antlr 321

Description: Deduction adding conjuncts to an antecedent.

Hypothesis

Ref	Expression
ad2ant.1	⊢ (φ → ψ)

Assertion

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

Proof of Theorem ad2antlr

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

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  tfindsg 2402  caoprord3 3072  oesuc 3134  oelim 3137  oaordi 3148  oaass 3163  oen0 3165  undom 3342  mapenlem1 3384  mapenlem2 3385  php3 3411  fiint 3445  fodom 3613  unxpdomlem 3649  npex 3885  elnp 3886  axnegex 4078  divneq0bt 4230  divdivdivt 4265  sqr11 4761  infxpidmlem12 4944  occont 5168  ocorth 5172  occllem6 5185  projlem25 5217  osumlem4 5533  5oalem1 5544  5oalem2 5545  3oalem2 5553  pjss2co 5634  pj3cor1 5661  atcvat3 5774  atcvat4 5775  mdsymlem5 5780

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