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  2660  vtocl3gf  2661  vtoclegft  2670  sbcthdv  2829  swopolem  4060  funssres  4962  fvmptssdm  5276  fmptcof  5352  fliftfuns  5458  isorel  5468  caovclg  5673  caovcomg  5676  caovassg  5679  caovcang  5682  caovordig  5686  caovordg  5688  caovdig  5695  caovdirg  5698  qliftfuns  6213  nneneq  6343  supmoti  6406  recexprlemopl  6815  recexprlemopu  6817  cauappcvgprlemladdrl  6847  caucvgsrlemcl  6965  caucvgsrlemfv  6967  caucvgsr  6978  lble  8025  uz11  8641  iseqfeq  9451  iseqcaopr3  9460  climcaucn  10188  dvdsprm  10518