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  4252  swopolem  4352  funssres  5313  fvmptssdm  5664  fmptcof  5747  fliftfuns  5867  isorel  5877  oveqrspc2v  5971  caovclg  6099  caovcomg  6102  caovassg  6105  caovcang  6108  caovordig  6112  caovordg  6114  caovdig  6121  caovdirg  6124  qliftfuns  6706  nneneq  6954  supmoti  7095  exmidonfinlem  7301  recexprlemopl  7738  recexprlemopu  7740  cauappcvgprlemladdrl  7770  caucvgsrlemcl  7902  caucvgsrlemfv  7904  caucvgsr  7915  suplocsrlempr  7920  ltordlem  8555  lble  9020  uz11  9671  seq3caopr3  10636  ccatass  11064  climcaucn  11662  sumdc  11669  fsum3  11698  fsumf1o  11701  fsum3cvg2  11705  isummulc2  11737  fsum2dlemstep  11745  fisumcom2  11749  fsumshftm  11756  fisum0diag2  11758  fsum00  11773  isumshft  11801  clim2prod  11850  prodmodclem2  11888  zproddc  11890  fprodseq  11894  fprodf1o  11899  prodssdc  11900  fprodm1s  11912  fprodp1s  11913  fprodcllemf  11924  fprodabs  11927  fprod2dlemstep  11933  fprodcom2fi  11937  dvdsprm  12459  pythagtriplem4  12591  pcmptdvds  12668  lidrididd  13214  grpidinv2  13390  ghmlin  13584  srgrz  13746  srglz  13747  ringinvnz1ne0  13811  rrgeq0i  14026  lmodlema  14054  islmodd  14055  lsslss  14143  ssnei2  14629  psmet0  14799  psmettri2  14800  cncfi  15050  dvcn  15172  dvmptfsum  15197  nninfsellemdc  15947