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  2885  vtocl3gf  2886  vtoclegft  2897  sbcthdv  3066  disji2  4117  exmid1stab  4340  swopolem  4445  funssres  5415  fvmptssdm  5784  fmptcof  5866  fliftfuns  5994  isorel  6004  oveqrspc2v  6102  caovclg  6232  caovcomg  6235  caovassg  6238  caovcang  6241  caovordig  6245  caovordg  6247  caovdig  6254  caovdirg  6257  qliftfuns  6883  nneneq  7148  supmoti  7323  exmidonfinlem  7535  recexprlemopl  7982  recexprlemopu  7984  cauappcvgprlemladdrl  8014  caucvgsrlemcl  8146  caucvgsrlemfv  8148  caucvgsr  8159  suplocsrlempr  8164  ltordlem  8800  lble  9267  uz11  9924  seq3caopr3  10906  hashfibclem  11260  ccatass  11354  swrdswrd  11455  swrdccatin1  11475  swrdccatin2  11479  climcaucn  12095  sumdc  12102  fsum3  12132  fsumf1o  12135  fsum3cvg2  12139  isummulc2  12171  fsum2dlemstep  12179  fisumcom2  12183  fsumshftm  12190  fisum0diag2  12192  fsum00  12207  isumshft  12235  clim2prod  12284  prodmodclem2  12322  zproddc  12324  fprodseq  12328  fprodf1o  12333  prodssdc  12334  fprodm1s  12346  fprodp1s  12347  fprodcllemf  12358  fprodabs  12361  fprod2dlemstep  12367  fprodcom2fi  12371  dvdsprm  12893  pythagtriplem4  13025  pcmptdvds  13102  lidrididd  13679  grpidinv2  13840  ghmlin  14028  srgrz  14262  srglz  14263  ringinvnz1ne0  14327  rrgeq0i  14545  lmodlema  14601  islmodd  14602  lsslss  14690  ssnei2  15181  psmet0  15351  psmettri2  15352  cncfi  15602  dvcn  15724  dvmptfsum  15749  usgruspgrben  16341  wlk1walkdom  16514  clwwlknonex2lem2  16593  nninfsellemdc  16958