Theorem anim12dan 882

Description: Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)

Hypotheses

Ref	Expression
anim12dan.1	|- ( ( ph /\ ps ) -> ch )
anim12dan.2	|- ( ( ph /\ th ) -> ta )

Assertion

Ref	Expression
anim12dan	|- ( ( ph /\ ( ps /\ th ) ) -> ( ch /\ ta ) )

Proof of Theorem anim12dan

Step	Hyp	Ref	Expression
1		anim12dan.1	. . . 4 |- ( ( ph /\ ps ) -> ch )
2	1	ex 450	. . 3 |- ( ph -> ( ps -> ch ) )
3		anim12dan.2	. . . 4 |- ( ( ph /\ th ) -> ta )
4	3	ex 450	. . 3 |- ( ph -> ( th -> ta ) )
5	2, 4	anim12d 586	. 2 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )
6	5	imp 445	1 |- ( ( ph /\ ( ps /\ th ) ) -> ( ch /\ ta ) )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  2f1fvneq  6517  isocnv  6580  isocnv3  6582  f1oiso2  6602  xpexr2  7107  f1o2ndf1  7285  fnwelem  7292  omword  7650  oeword  7670  swoso  7775  xpf1o  8122  zorn2lem6  9323  ltapr  9867  ltord1  10554  pc11  15584  imasaddfnlem  16188  imasaddflem  16190  pslem  17206  mhmpropd  17341  frmdsssubm  17398  ghmsub  17668  gasubg  17735  invrpropd  18698  mplcoe5lem  19467  evlseu  19516  znfld  19909  cygznlem3  19918  cpmatmcl  20524  tgclb  20774  innei  20929  txcn  21429  txflf  21810  qustgplem  21924  clmsub4  22906  cfilresi  23093  volcn  23374  itg1addlem4  23466  dvlip  23756  plymullem1  23970  lgsdir2  25055  lgsdchr  25080  brbtwn2  25785  axcontlem7  25850  frgrncvvdeqlem8  27170  nvaddsub4  27512  hhcno  28763  hhcnf  28764  unopf1o  28775  counop  28780  afsval  30749  ontopbas  32427  onsuct0  32440  heicant  33444  ftc1anclem6  33490  anim12da  33506  equivbnd2  33591  ismtybndlem  33605  ismrer1  33637  iccbnd  33639  xihopellsmN  36543  dihopellsm  36544  dvconstbi  38533  fargshiftf1  41377  mgmhmpropd  41785  elpglem1  42454