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  2838  cgsex2g  2839  cgsex4g  2840  reximdva0m  3510  difsn  3810  preq12b  3853  elres  5049  relssres  5051  fnoprabg  6121  1idprl  7809  1idpru  7810  msqge0  8795  mulge0  8798  fzospliti  10412  algcvga  12622  prmind2  12691  sqrt2irr  12733  grpinveu  13620  metrest  15229  2sqlem10  15853  clwwlkn1loopb  16270