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	|- ( ph -> ps )
mpan9.2	|- ( ch -> ( ps -> th ) )

Assertion

Ref	Expression
mpan9	|- ( ( ph /\ ch ) -> th )

Proof of Theorem mpan9

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 |- ( ph -> ps )
2		mpan9.2	. . 3 |- ( ch -> ( ps -> th ) )
3	1, 2	syl5 32	. 2 |- ( ch -> ( ph -> th ) )
4	3	impcom 124	1 |- ( ( ph /\ ch ) -> th )

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  2787  vtocl3gf  2788  vtoclegft  2797  sbcthdv  2964  disji2  3974  swopolem  4282  funssres  5229  fvmptssdm  5569  fmptcof  5651  fliftfuns  5765  isorel  5775  caovclg  5990  caovcomg  5993  caovassg  5996  caovcang  5999  caovordig  6003  caovordg  6005  caovdig  6012  caovdirg  6015  qliftfuns  6581  nneneq  6819  supmoti  6954  exmidonfinlem  7145  recexprlemopl  7562  recexprlemopu  7564  cauappcvgprlemladdrl  7594  caucvgsrlemcl  7726  caucvgsrlemfv  7728  caucvgsr  7739  suplocsrlempr  7744  ltordlem  8376  lble  8838  uz11  9484  seq3caopr3  10412  climcaucn  11288  sumdc  11295  fsum3  11324  fsumf1o  11327  fsum3cvg2  11331  isummulc2  11363  fsum2dlemstep  11371  fisumcom2  11375  fsumshftm  11382  fisum0diag2  11384  fsum00  11399  isumshft  11427  clim2prod  11476  prodmodclem2  11514  zproddc  11516  fprodseq  11520  fprodf1o  11525  prodssdc  11526  fprodm1s  11538  fprodp1s  11539  fprodcllemf  11550  fprodabs  11553  fprod2dlemstep  11559  fprodcom2fi  11563  dvdsprm  12065  pythagtriplem4  12196  pcmptdvds  12271  ssnei2  12757  psmet0  12927  psmettri2  12928  cncfi  13165  dvcn  13264  exmid1stab  13840  nninfsellemdc  13850