Theorem mpan9 279

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 124	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  sylan  281  vtocl2gf  2788  vtocl3gf  2789  vtoclegft  2798  sbcthdv  2965  disji2  3975  swopolem  4283  funssres  5230  fvmptssdm  5570  fmptcof  5652  fliftfuns  5766  isorel  5776  oveqrspc2v  5869  caovclg  5994  caovcomg  5997  caovassg  6000  caovcang  6003  caovordig  6007  caovordg  6009  caovdig  6016  caovdirg  6019  qliftfuns  6585  nneneq  6823  supmoti  6958  exmidonfinlem  7149  recexprlemopl  7566  recexprlemopu  7568  cauappcvgprlemladdrl  7598  caucvgsrlemcl  7730  caucvgsrlemfv  7732  caucvgsr  7743  suplocsrlempr  7748  ltordlem  8380  lble  8842  uz11  9488  seq3caopr3  10416  climcaucn  11292  sumdc  11299  fsum3  11328  fsumf1o  11331  fsum3cvg2  11335  isummulc2  11367  fsum2dlemstep  11375  fisumcom2  11379  fsumshftm  11386  fisum0diag2  11388  fsum00  11403  isumshft  11431  clim2prod  11480  prodmodclem2  11518  zproddc  11520  fprodseq  11524  fprodf1o  11529  prodssdc  11530  fprodm1s  11542  fprodp1s  11543  fprodcllemf  11554  fprodabs  11557  fprod2dlemstep  11563  fprodcom2fi  11567  dvdsprm  12069  pythagtriplem4  12200  pcmptdvds  12275  lidrididd  12613  ssnei2  12807  psmet0  12977  psmettri2  12978  cncfi  13215  dvcn  13314  exmid1stab  13890  nninfsellemdc  13900