Theorem mp3an2i 1320

Description: mp3an 1315 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 1302	. 2 |- ( ( ch /\ th ) -> ta )
6	1, 2, 5	syl2anc 408	1 |- ( ps -> ta )

Syntax hints:   -> wi 4   /\ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  mapen  6740  mapxpen  6742  en2eleq  7051  nnledivrp  9553  xsubge0  9664  frec2uzsucd  10174  seq3shft  10610  geolim2  11281  geoisum1c  11289  ntrivcvgap  11317  eflegeo  11408  sin01gt0  11468  cos01gt0  11469  gcdn0gt0  11666  divgcdodd  11821  sqpweven  11853  2sqpwodd  11854  ressid  12020  topnvalg  12132  restbasg  12337  restco  12343  lmfval  12361  cnfval  12363  cnpval  12367  upxp  12441  uptx  12443  txrest  12445  xblm  12586  bdmet  12671  bdmopn  12673  reopnap  12707  cnopnap  12763  dvidlemap  12829  dvcj  12842  trilpolemisumle  13231