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  5101  relssres  5103  fnoprabg  6192  1idprl  7963  1idpru  7964  msqge0  8952  mulge0  8955  fzospliti  10601  algcvga  12853  prmind2  12922  sqrt2irr  12965  grpinveu  13901  metrest  15749  chtqub  16313  2sqlem10  16466  clwwlkn1loopb  16883