Theorem mp3an2i 1342

Description: mp3an 1337 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses

Ref	Expression
mp3an2i.1	|- ph
mp3an2i.2	|- ( ps -> ch )
mp3an2i.3	|- ( ps -> th )
mp3an2i.4	|- ( ( ph /\ ch /\ th ) -> ta )

Assertion

Ref	Expression
mp3an2i	|- ( ps -> ta )

Proof of Theorem mp3an2i

Step	Hyp	Ref	Expression
1		mp3an2i.2	. 2 |- ( ps -> ch )
2		mp3an2i.3	. 2 |- ( ps -> th )
3		mp3an2i.1	. . 3 |- ph
4		mp3an2i.4	. . 3 |- ( ( ph /\ ch /\ th ) -> ta )
5	3, 4	mp3an1 1324	. 2 |- ( ( ch /\ th ) -> ta )
6	1, 2, 5	syl2anc 411	1 |- ( ps -> ta )

Syntax hints:   -> wi 4   /\ w3a 978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  mapen  6846  mapxpen  6848  en2eleq  7194  nnledivrp  9766  xsubge0  9881  iccen  10006  frec2uzsucd  10401  seq3shft  10847  geolim2  11520  geoisum1c  11528  ntrivcvgap  11556  eflegeo  11709  sin01gt0  11769  cos01gt0  11770  gcdn0gt0  11979  uzwodc  12038  divgcdodd  12143  sqpweven  12175  2sqpwodd  12176  pythagtriplem4  12268  pythagtriplem11  12274  pythagtriplem12  12275  pythagtriplem13  12276  pythagtriplem14  12277  pcfac  12348  omctfn  12444  ssnnctlemct  12447  topnvalg  12700  imasmulr  12730  imasaddfnlemg  12735  ismhm  12853  scaffng  13399  zringinvg  13497  restbasg  13671  restco  13677  lmfval  13695  cnfval  13697  cnpval  13701  upxp  13775  uptx  13777  txrest  13779  xblm  13920  bdmet  14005  bdmopn  14007  reopnap  14041  cnopnap  14097  dvidlemap  14163  dvcj  14176  eflt  14199  logdivlti  14305  trilpolemisumle  14789