Theorem ancld 323

Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)

Hypothesis

Ref	Expression
ancld.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ancld	⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒)))

Proof of Theorem ancld

Step	Hyp	Ref	Expression
1		idd 21	. 2 ⊢ (𝜑 → (𝜓 → 𝜓))
2		ancld.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	jcad 305	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mopick2  2082  cgsexg  2721  cgsex2g  2722  cgsex4g  2723  reximdva0m  3378  difsn  3657  preq12b  3697  elres  4855  relssres  4857  fnoprabg  5872  1idprl  7398  1idpru  7399  msqge0  8378  mulge0  8381  fzospliti  9953  algcvga  11732  prmind2  11801  sqrt2irr  11840  metrest  12675