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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mopick2  2170  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  reximdva0m  3537  difsn  3852  preq12b  3895  elres  5099  relssres  5101  fnoprabg  6189  1idprl  7957  1idpru  7958  msqge0  8946  mulge0  8949  fzospliti  10595  algcvga  12845  prmind2  12914  sqrt2irr  12957  grpinveu  13892  metrest  15656  2sqlem10  16342  clwwlkn1loopb  16759