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  2163  cgsexg  2839  cgsex2g  2840  cgsex4g  2841  reximdva0m  3512  difsn  3815  preq12b  3858  elres  5055  relssres  5057  fnoprabg  6132  1idprl  7853  1idpru  7854  msqge0  8838  mulge0  8841  fzospliti  10458  algcvga  12686  prmind2  12755  sqrt2irr  12797  grpinveu  13684  metrest  15300  2sqlem10  15927  clwwlkn1loopb  16344