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  2867  vtocl3gf  2868  vtoclegft  2879  sbcthdv  3047  disji2  4085  exmid1stab  4304  swopolem  4408  funssres  5376  fvmptssdm  5740  fmptcof  5822  fliftfuns  5949  isorel  5959  oveqrspc2v  6055  caovclg  6185  caovcomg  6188  caovassg  6191  caovcang  6194  caovordig  6198  caovordg  6200  caovdig  6207  caovdirg  6210  qliftfuns  6831  nneneq  7086  supmoti  7252  exmidonfinlem  7464  recexprlemopl  7905  recexprlemopu  7907  cauappcvgprlemladdrl  7937  caucvgsrlemcl  8069  caucvgsrlemfv  8071  caucvgsr  8082  suplocsrlempr  8087  ltordlem  8721  lble  9186  uz11  9840  seq3caopr3  10816  ccatass  11251  swrdswrd  11352  swrdccatin1  11372  swrdccatin2  11376  climcaucn  11991  sumdc  11998  fsum3  12028  fsumf1o  12031  fsum3cvg2  12035  isummulc2  12067  fsum2dlemstep  12075  fisumcom2  12079  fsumshftm  12086  fisum0diag2  12088  fsum00  12103  isumshft  12131  clim2prod  12180  prodmodclem2  12218  zproddc  12220  fprodseq  12224  fprodf1o  12229  prodssdc  12230  fprodm1s  12242  fprodp1s  12243  fprodcllemf  12254  fprodabs  12257  fprod2dlemstep  12263  fprodcom2fi  12267  dvdsprm  12789  pythagtriplem4  12921  pcmptdvds  12998  lidrididd  13545  grpidinv2  13721  ghmlin  13915  srgrz  14078  srglz  14079  ringinvnz1ne0  14143  rrgeq0i  14359  lmodlema  14388  islmodd  14389  lsslss  14477  ssnei2  14968  psmet0  15138  psmettri2  15139  cncfi  15389  dvcn  15511  dvmptfsum  15536  usgruspgrben  16127  wlk1walkdom  16300  clwwlknonex2lem2  16379  nninfsellemdc  16736