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  2866  vtocl3gf  2867  vtoclegft  2878  sbcthdv  3046  disji2  4080  exmid1stab  4298  swopolem  4402  funssres  5369  fvmptssdm  5731  fmptcof  5814  fliftfuns  5939  isorel  5949  oveqrspc2v  6045  caovclg  6175  caovcomg  6178  caovassg  6181  caovcang  6184  caovordig  6188  caovordg  6190  caovdig  6197  caovdirg  6200  qliftfuns  6788  nneneq  7043  supmoti  7192  exmidonfinlem  7404  recexprlemopl  7845  recexprlemopu  7847  cauappcvgprlemladdrl  7877  caucvgsrlemcl  8009  caucvgsrlemfv  8011  caucvgsr  8022  suplocsrlempr  8027  ltordlem  8662  lble  9127  uz11  9779  seq3caopr3  10754  ccatass  11189  swrdswrd  11290  swrdccatin1  11310  swrdccatin2  11314  climcaucn  11929  sumdc  11936  fsum3  11966  fsumf1o  11969  fsum3cvg2  11973  isummulc2  12005  fsum2dlemstep  12013  fisumcom2  12017  fsumshftm  12024  fisum0diag2  12026  fsum00  12041  isumshft  12069  clim2prod  12118  prodmodclem2  12156  zproddc  12158  fprodseq  12162  fprodf1o  12167  prodssdc  12168  fprodm1s  12180  fprodp1s  12181  fprodcllemf  12192  fprodabs  12195  fprod2dlemstep  12201  fprodcom2fi  12205  dvdsprm  12727  pythagtriplem4  12859  pcmptdvds  12936  lidrididd  13483  grpidinv2  13659  ghmlin  13853  srgrz  14016  srglz  14017  ringinvnz1ne0  14081  rrgeq0i  14297  lmodlema  14325  islmodd  14326  lsslss  14414  ssnei2  14900  psmet0  15070  psmettri2  15071  cncfi  15321  dvcn  15443  dvmptfsum  15468  usgruspgrben  16056  wlk1walkdom  16229  clwwlknonex2lem2  16308  nninfsellemdc  16663