Theorem mp3an2i 1383

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mapsnend  7099  mapen  7146  mapxpen  7148  mapunen  7151  en2eleq  7548  nnledivrp  10178  xsubge0  10294  iccen  10420  fzen  10458  fldiv4lem1div2uz2  10756  frec2uzsucd  10853  seqp1g  10918  fnpfx  11465  cats1fvn  11552  seq3shft  11619  geolim2  12298  geoisum1c  12306  ntrivcvgap  12334  eflegeo  12487  sin01gt0  12548  cos01gt0  12549  3dvds  12650  gcdn0gt0  12774  uzwodc  12833  divgcdodd  12941  sqpweven  12974  2sqpwodd  12975  pythagtriplem4  13070  pythagtriplem11  13076  pythagtriplem12  13077  pythagtriplem13  13078  pythagtriplem14  13079  pcfac  13152  4sqlemffi  13198  ballotfilemfcc  13285  ballotfilemfmpn  13286  omctfn  13386  ssnnctlemct  13389  topnvalg  13658  imasmulr  13683  imasaddfnlemg  13688  gzsumsplit1r  13768  ismhm  13821  mhmex  13822  gsumvalfi  14236  prdsinvlem  14280  scaffng  14730  lss1d  14804  zringinvg  15023  psrplusgg  15154  psrmulrg  15158  restbasg  15360  restco  15366  lmfval  15385  cnfval  15386  cnpval  15390  upxp  15464  uptx  15466  txrest  15468  xblm  15609  bdmet  15694  bdmopn  15696  reopnap  15738  cnopnap  15803  maxcncf  15807  mincncf  15808  dvidlemap  15883  dvcj  15901  plyval  15924  plysub  15945  eflt  15967  logdivlti  16075  log2tlbndlog2  16181  perfectlem1  16260  perfectlem2  16261  gausslemma2dlem0i  16342  gausslemma2dlem4  16349  lgsquad2lem1  16366  lgsquad2lem2  16367  clwwlknon  16836  trilpolemisumle  17254