Theorem mp3an2i 1321

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

Syntax hints:   -> wi 4   /\ w3a 963

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 965

This theorem is referenced by:  mapen  6748  mapxpen  6750  en2eleq  7068  nnledivrp  9583  xsubge0  9694  iccen  9819  frec2uzsucd  10205  seq3shft  10642  geolim2  11313  geoisum1c  11321  ntrivcvgap  11349  eflegeo  11444  sin01gt0  11504  cos01gt0  11505  gcdn0gt0  11702  divgcdodd  11857  sqpweven  11889  2sqpwodd  11890  omctfn  11992  ressid  12059  topnvalg  12171  restbasg  12376  restco  12382  lmfval  12400  cnfval  12402  cnpval  12406  upxp  12480  uptx  12482  txrest  12484  xblm  12625  bdmet  12710  bdmopn  12712  reopnap  12746  cnopnap  12802  dvidlemap  12868  dvcj  12881  eflt  12904  logdivlti  13010  trilpolemisumle  13406