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  2164  cgsexg  2849  cgsex2g  2850  cgsex4g  2851  reximdva0m  3524  difsn  3831  preq12b  3874  elres  5074  relssres  5076  fnoprabg  6154  1idprl  7905  1idpru  7906  msqge0  8890  mulge0  8893  fzospliti  10512  algcvga  12748  prmind2  12817  sqrt2irr  12859  grpinveu  13751  metrest  15371  2sqlem10  15998  clwwlkn1loopb  16415