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  6848  mapxpen  6850  en2eleq  7196  nnledivrp  9768  xsubge0  9883  iccen  10008  frec2uzsucd  10403  seq3shft  10849  geolim2  11522  geoisum1c  11530  ntrivcvgap  11558  eflegeo  11711  sin01gt0  11771  cos01gt0  11772  gcdn0gt0  11981  uzwodc  12040  divgcdodd  12145  sqpweven  12177  2sqpwodd  12178  pythagtriplem4  12270  pythagtriplem11  12276  pythagtriplem12  12277  pythagtriplem13  12278  pythagtriplem14  12279  pcfac  12350  omctfn  12446  ssnnctlemct  12449  topnvalg  12705  imasmulr  12735  imasaddfnlemg  12740  ismhm  12858  scaffng  13404  lss1d  13475  zringinvg  13579  restbasg  13753  restco  13759  lmfval  13777  cnfval  13779  cnpval  13783  upxp  13857  uptx  13859  txrest  13861  xblm  14002  bdmet  14087  bdmopn  14089  reopnap  14123  cnopnap  14179  dvidlemap  14245  dvcj  14258  eflt  14281  logdivlti  14387  trilpolemisumle  14871