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  2864  vtocl3gf  2865  vtoclegft  2876  sbcthdv  3044  disji2  4078  exmid1stab  4296  swopolem  4400  funssres  5366  fvmptssdm  5727  fmptcof  5810  fliftfuns  5934  isorel  5944  oveqrspc2v  6040  caovclg  6170  caovcomg  6173  caovassg  6176  caovcang  6179  caovordig  6183  caovordg  6185  caovdig  6192  caovdirg  6195  qliftfuns  6783  nneneq  7038  supmoti  7183  exmidonfinlem  7394  recexprlemopl  7835  recexprlemopu  7837  cauappcvgprlemladdrl  7867  caucvgsrlemcl  7999  caucvgsrlemfv  8001  caucvgsr  8012  suplocsrlempr  8017  ltordlem  8652  lble  9117  uz11  9769  seq3caopr3  10743  ccatass  11175  swrdswrd  11276  swrdccatin1  11296  swrdccatin2  11300  climcaucn  11902  sumdc  11909  fsum3  11938  fsumf1o  11941  fsum3cvg2  11945  isummulc2  11977  fsum2dlemstep  11985  fisumcom2  11989  fsumshftm  11996  fisum0diag2  11998  fsum00  12013  isumshft  12041  clim2prod  12090  prodmodclem2  12128  zproddc  12130  fprodseq  12134  fprodf1o  12139  prodssdc  12140  fprodm1s  12152  fprodp1s  12153  fprodcllemf  12164  fprodabs  12167  fprod2dlemstep  12173  fprodcom2fi  12177  dvdsprm  12699  pythagtriplem4  12831  pcmptdvds  12908  lidrididd  13455  grpidinv2  13631  ghmlin  13825  srgrz  13987  srglz  13988  ringinvnz1ne0  14052  rrgeq0i  14268  lmodlema  14296  islmodd  14297  lsslss  14385  ssnei2  14871  psmet0  15041  psmettri2  15042  cncfi  15292  dvcn  15414  dvmptfsum  15439  usgruspgrben  16025  wlk1walkdom  16156  clwwlknonex2lem2  16233  nninfsellemdc  16548