Theorem mpan9 455

Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpan9.1	⊢ (φ → ψ)
mpan9.2	⊢ (χ → (ψ → θ))

Assertion

Ref	Expression
mpan9	⊢ ((φ ∧ χ) → θ)

Proof of Theorem mpan9

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 ⊢ (φ → ψ)
2		mpan9.2	. . 3 ⊢ (χ → (ψ → θ))
3	1, 2	syl5 28	. 2 ⊢ (χ → (φ → θ))
4	3	impcom 419	1 ⊢ ((φ ∧ χ) → θ)

Syntax hints:   → wi 4   ∧ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  sylan  457  vtocl2gf  2917  vtocl3gf  2918  vtoclegft  2927  sbcthdv  3062  nnsucelr  4429  nnadjoin  4521  sfintfin  4533  funiunfv  5468  isorel  5490  caovcld  5623  caovcomg  5625  caovassg  5627  caovdig  5633  caovdirg  5634