Theorem anim12dan 835

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 432	. . 3 |- ( ph -> ( ps -> ch ) )
3		anim12dan.2	. . . 4 |- ( ( ph /\ th ) -> ta )
4	3	ex 432	. . 3 |- ( ph -> ( th -> ta ) )
5	2, 4	anim12d 561	. 2 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )
6	5	imp 427	1 |- ( ( ph /\ ( ps /\ th ) ) -> ( ch /\ ta ) )

Syntax hints:   -> wi 4   /\ wa 367

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 185  df-an 369

This theorem is referenced by:  isocnv  6201  isocnv3  6203  f1oiso2  6223  xpexr2  6714  f1o2ndf1  6881  fnwelem  6888  omword  7211  oeword  7231  swoso  7334  xpf1o  7672  zorn2lem6  8872  ltapr  9412  ltord1  10075  pc11  14487  imasaddfnlem  15017  imasaddflem  15019  pslem  16035  mhmpropd  16171  frmdsssubm  16228  ghmsub  16474  gasubg  16539  invrpropd  17542  mplcoe5lem  18325  evlseu  18380  znfld  18772  cygznlem3  18781  cpmatmcl  19387  tgclb  19639  innei  19793  txcn  20293  txflf  20673  qustgplem  20785  cfilresi  21900  volcn  22181  itg1addlem4  22272  dvlip  22560  plymullem1  22777  lgsdir2  23801  lgsdchr  23821  brbtwn2  24410  axcontlem7  24475  usgra2adedgwlkon  24817  fargshiftf1  24839  frgrancvvdeqlemB  25240  ghgrplem2OLD  25567  ghsubgolemOLD  25570  vcsub4  25667  nvaddsub4  25754  hhcno  27021  hhcnf  27022  unopf1o  27033  counop  27038  afsval  28815  ghomgsg  29297  ontopbas  30121  onsuct0  30134  heicant  30289  ftc1anclem6  30335  anim12da  30441  equivbnd2  30528  ismtybndlem  30542  ismrer1  30574  iccbnd  30576  dvconstbi  31480  2f1fvneq  32681  mgmhmpropd  32845  xihopellsmN  37378  dihopellsm  37379