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	|- ( 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 125	1 |- ( ( ph /\ ch ) -> th )

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  2835  vtocl3gf  2836  vtoclegft  2845  sbcthdv  3013  disji2  4037  exmid1stab  4253  swopolem  4353  funssres  5314  fvmptssdm  5666  fmptcof  5749  fliftfuns  5869  isorel  5879  oveqrspc2v  5973  caovclg  6101  caovcomg  6104  caovassg  6107  caovcang  6110  caovordig  6114  caovordg  6116  caovdig  6123  caovdirg  6126  qliftfuns  6708  nneneq  6956  supmoti  7097  exmidonfinlem  7303  recexprlemopl  7740  recexprlemopu  7742  cauappcvgprlemladdrl  7772  caucvgsrlemcl  7904  caucvgsrlemfv  7906  caucvgsr  7917  suplocsrlempr  7922  ltordlem  8557  lble  9022  uz11  9673  seq3caopr3  10638  ccatass  11067  climcaucn  11695  sumdc  11702  fsum3  11731  fsumf1o  11734  fsum3cvg2  11738  isummulc2  11770  fsum2dlemstep  11778  fisumcom2  11782  fsumshftm  11789  fisum0diag2  11791  fsum00  11806  isumshft  11834  clim2prod  11883  prodmodclem2  11921  zproddc  11923  fprodseq  11927  fprodf1o  11932  prodssdc  11933  fprodm1s  11945  fprodp1s  11946  fprodcllemf  11957  fprodabs  11960  fprod2dlemstep  11966  fprodcom2fi  11970  dvdsprm  12492  pythagtriplem4  12624  pcmptdvds  12701  lidrididd  13247  grpidinv2  13423  ghmlin  13617  srgrz  13779  srglz  13780  ringinvnz1ne0  13844  rrgeq0i  14059  lmodlema  14087  islmodd  14088  lsslss  14176  ssnei2  14662  psmet0  14832  psmettri2  14833  cncfi  15083  dvcn  15205  dvmptfsum  15230  nninfsellemdc  15984