Theorem mpan9 281

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  sylan  283  vtocl2gf  2826  vtocl3gf  2827  vtoclegft  2836  sbcthdv  3004  disji2  4026  exmid1stab  4241  swopolem  4340  funssres  5300  fvmptssdm  5646  fmptcof  5729  fliftfuns  5845  isorel  5855  oveqrspc2v  5949  caovclg  6076  caovcomg  6079  caovassg  6082  caovcang  6085  caovordig  6089  caovordg  6091  caovdig  6098  caovdirg  6101  qliftfuns  6678  nneneq  6918  supmoti  7059  exmidonfinlem  7260  recexprlemopl  7692  recexprlemopu  7694  cauappcvgprlemladdrl  7724  caucvgsrlemcl  7856  caucvgsrlemfv  7858  caucvgsr  7869  suplocsrlempr  7874  ltordlem  8509  lble  8974  uz11  9624  seq3caopr3  10583  climcaucn  11516  sumdc  11523  fsum3  11552  fsumf1o  11555  fsum3cvg2  11559  isummulc2  11591  fsum2dlemstep  11599  fisumcom2  11603  fsumshftm  11610  fisum0diag2  11612  fsum00  11627  isumshft  11655  clim2prod  11704  prodmodclem2  11742  zproddc  11744  fprodseq  11748  fprodf1o  11753  prodssdc  11754  fprodm1s  11766  fprodp1s  11767  fprodcllemf  11778  fprodabs  11781  fprod2dlemstep  11787  fprodcom2fi  11791  dvdsprm  12305  pythagtriplem4  12437  pcmptdvds  12514  lidrididd  13025  grpidinv2  13190  ghmlin  13378  srgrz  13540  srglz  13541  ringinvnz1ne0  13605  rrgeq0i  13820  lmodlema  13848  islmodd  13849  lsslss  13937  ssnei2  14393  psmet0  14563  psmettri2  14564  cncfi  14814  dvcn  14936  dvmptfsum  14961  nninfsellemdc  15654