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  6733  mapxpen  6735  en2eleq  7044  nnledivrp  9546  xsubge0  9657  frec2uzsucd  10167  seq3shft  10603  geolim2  11274  geoisum1c  11282  ntrivcvgap  11310  eflegeo  11397  sin01gt0  11457  cos01gt0  11458  gcdn0gt0  11655  divgcdodd  11810  sqpweven  11842  2sqpwodd  11843  ressid  12009  topnvalg  12121  restbasg  12326  restco  12332  lmfval  12350  cnfval  12352  cnpval  12356  upxp  12430  uptx  12432  txrest  12434  xblm  12575  bdmet  12660  bdmopn  12662  reopnap  12696  cnopnap  12752  dvidlemap  12818  dvcj  12831  trilpolemisumle  13220