Theorem ancld 325

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 307	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  mopick2  2161  cgsexg  2836  cgsex2g  2837  cgsex4g  2838  reximdva0m  3508  difsn  3808  preq12b  3851  elres  5047  relssres  5049  fnoprabg  6117  1idprl  7800  1idpru  7801  msqge0  8786  mulge0  8789  fzospliti  10403  algcvga  12613  prmind2  12682  sqrt2irr  12724  grpinveu  13611  metrest  15220  2sqlem10  15844  clwwlkn1loopb  16215