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  2840  vtocl3gf  2841  vtoclegft  2852  sbcthdv  3020  disji2  4051  exmid1stab  4268  swopolem  4370  funssres  5332  fvmptssdm  5687  fmptcof  5770  fliftfuns  5890  isorel  5900  oveqrspc2v  5994  caovclg  6122  caovcomg  6125  caovassg  6128  caovcang  6131  caovordig  6135  caovordg  6137  caovdig  6144  caovdirg  6147  qliftfuns  6729  nneneq  6979  supmoti  7121  exmidonfinlem  7332  recexprlemopl  7773  recexprlemopu  7775  cauappcvgprlemladdrl  7805  caucvgsrlemcl  7937  caucvgsrlemfv  7939  caucvgsr  7950  suplocsrlempr  7955  ltordlem  8590  lble  9055  uz11  9706  seq3caopr3  10673  ccatass  11102  swrdswrd  11196  swrdccatin1  11216  swrdccatin2  11220  climcaucn  11777  sumdc  11784  fsum3  11813  fsumf1o  11816  fsum3cvg2  11820  isummulc2  11852  fsum2dlemstep  11860  fisumcom2  11864  fsumshftm  11871  fisum0diag2  11873  fsum00  11888  isumshft  11916  clim2prod  11965  prodmodclem2  12003  zproddc  12005  fprodseq  12009  fprodf1o  12014  prodssdc  12015  fprodm1s  12027  fprodp1s  12028  fprodcllemf  12039  fprodabs  12042  fprod2dlemstep  12048  fprodcom2fi  12052  dvdsprm  12574  pythagtriplem4  12706  pcmptdvds  12783  lidrididd  13329  grpidinv2  13505  ghmlin  13699  srgrz  13861  srglz  13862  ringinvnz1ne0  13926  rrgeq0i  14141  lmodlema  14169  islmodd  14170  lsslss  14258  ssnei2  14744  psmet0  14914  psmettri2  14915  cncfi  15165  dvcn  15287  dvmptfsum  15312  nninfsellemdc  16149