Theorem anc2li 302

Description: Deduction conjoining antecedent to left of consequent in nested implication.

Hypothesis

Ref	Expression
anc2li.1	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
anc2li	⊢ (φ → (ψ → (φ ⋀ χ)))

Proof of Theorem anc2li

Step	Hyp	Ref	Expression
1		anc2li.1	. 2 ⊢ (φ → (ψ → χ))
2		anc2l 300	. 2 ⊢ ((φ → (ψ → χ)) → (φ → (ψ → (φ ⋀ χ))))
3	1, 2	ax-mp 7	1 ⊢ (φ → (ψ → (φ ⋀ χ)))

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  imdistani 443  equvini 1166  pwpw0 2465  sssn 2469  opprc3 2792  tfis 3122  oeordi 4204  unblem3 4525  trcl 4625  rankr1 4654  ac5b 4733  sqr2irr 6667  metelcls 7916  h1datom 9444

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain