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  2863  vtocl3gf  2864  vtoclegft  2875  sbcthdv  3043  disji2  4075  exmid1stab  4292  swopolem  4396  funssres  5360  fvmptssdm  5721  fmptcof  5804  fliftfuns  5928  isorel  5938  oveqrspc2v  6034  caovclg  6164  caovcomg  6167  caovassg  6170  caovcang  6173  caovordig  6177  caovordg  6179  caovdig  6186  caovdirg  6189  qliftfuns  6774  nneneq  7026  supmoti  7171  exmidonfinlem  7382  recexprlemopl  7823  recexprlemopu  7825  cauappcvgprlemladdrl  7855  caucvgsrlemcl  7987  caucvgsrlemfv  7989  caucvgsr  8000  suplocsrlempr  8005  ltordlem  8640  lble  9105  uz11  9757  seq3caopr3  10725  ccatass  11156  swrdswrd  11253  swrdccatin1  11273  swrdccatin2  11277  climcaucn  11878  sumdc  11885  fsum3  11914  fsumf1o  11917  fsum3cvg2  11921  isummulc2  11953  fsum2dlemstep  11961  fisumcom2  11965  fsumshftm  11972  fisum0diag2  11974  fsum00  11989  isumshft  12017  clim2prod  12066  prodmodclem2  12104  zproddc  12106  fprodseq  12110  fprodf1o  12115  prodssdc  12116  fprodm1s  12128  fprodp1s  12129  fprodcllemf  12140  fprodabs  12143  fprod2dlemstep  12149  fprodcom2fi  12153  dvdsprm  12675  pythagtriplem4  12807  pcmptdvds  12884  lidrididd  13431  grpidinv2  13607  ghmlin  13801  srgrz  13963  srglz  13964  ringinvnz1ne0  14028  rrgeq0i  14244  lmodlema  14272  islmodd  14273  lsslss  14361  ssnei2  14847  psmet0  15017  psmettri2  15018  cncfi  15268  dvcn  15390  dvmptfsum  15415  usgruspgrben  16000  wlk1walkdom  16105  nninfsellemdc  16464