Theorem mp3an2i 1324

Description: mp3an 1319 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 1306	. 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  6788  mapxpen  6790  en2eleq  7125  nnledivrp  9668  xsubge0  9780  iccen  9905  frec2uzsucd  10295  seq3shft  10733  geolim2  11404  geoisum1c  11412  ntrivcvgap  11440  eflegeo  11593  sin01gt0  11653  cos01gt0  11654  gcdn0gt0  11856  divgcdodd  12012  sqpweven  12044  2sqpwodd  12045  omctfn  12159  ssnnctlemct  12162  ressid  12238  topnvalg  12350  restbasg  12555  restco  12561  lmfval  12579  cnfval  12581  cnpval  12585  upxp  12659  uptx  12661  txrest  12663  xblm  12804  bdmet  12889  bdmopn  12891  reopnap  12925  cnopnap  12981  dvidlemap  13047  dvcj  13060  eflt  13083  logdivlti  13189  trilpolemisumle  13596