Theorem mpan9 275

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 32	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 123	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105

This theorem is referenced by:  sylan  277  vtocl2gf  2661  vtocl3gf  2662  vtoclegft  2671  sbcthdv  2830  swopolem  4068  funssres  4972  fvmptssdm  5287  fmptcof  5363  fliftfuns  5469  isorel  5479  caovclg  5684  caovcomg  5687  caovassg  5690  caovcang  5693  caovordig  5697  caovordg  5699  caovdig  5706  caovdirg  5709  qliftfuns  6256  nneneq  6392  supmoti  6465  recexprlemopl  6877  recexprlemopu  6879  cauappcvgprlemladdrl  6909  caucvgsrlemcl  7027  caucvgsrlemfv  7029  caucvgsr  7040  lble  8092  uz11  8722  iseqfeq  9547  iseqcaopr3  9556  climcaucn  10326  sumdc  10333  dvdsprm  10662