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  2166  cgsexg  2851  cgsex2g  2852  cgsex4g  2853  reximdva0m  3528  difsn  3836  preq12b  3879  elres  5079  relssres  5081  fnoprabg  6162  1idprl  7921  1idpru  7922  msqge0  8908  mulge0  8911  fzospliti  10537  algcvga  12777  prmind2  12846  sqrt2irr  12888  grpinveu  13797  metrest  15501  2sqlem10  16128  clwwlkn1loopb  16545