Theorem anim12dan 834

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

Syntax hints:   -> wi 4   /\ wa 369

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 371

This theorem is referenced by:  isocnv  6207  isocnv3  6209  f1oiso2  6229  xpexr2  6717  f1o2ndf1  6883  fnwelem  6890  omword  7211  oeword  7231  swoso  7334  xpf1o  7671  zorn2lem6  8872  ltapr  9414  ltord1  10070  pc11  14253  imasaddfnlem  14774  imasaddflem  14776  pslem  15684  mhmpropd  15778  frmdsssubm  15847  ghmsub  16065  gasubg  16130  invrpropd  17126  mplcoe5lem  17896  evlseu  17951  znfld  18361  cygznlem3  18370  cpmatmcl  18982  tgclb  19233  innei  19387  txcn  19857  txflf  20237  divstgplem  20349  cfilresi  21464  volcn  21745  itg1addlem4  21836  dvlip  22124  plymullem1  22341  lgsdir2  23326  lgsdchr  23346  brbtwn2  23879  axcontlem7  23944  usgra2adedgwlkon  24279  fargshiftf1  24301  frgrancvvdeqlemB  24703  ghgrplem2  25033  ghsubgolem  25036  vcsub4  25133  nvaddsub4  25220  hhcno  26487  hhcnf  26488  unopf1o  26499  counop  26504  ghomgsg  28496  ontopbas  29458  onsuct0  29471  heicant  29615  ftc1anclem6  29661  anim12da  29793  equivbnd2  29880  ismtybndlem  29894  ismrer1  29926  iccbnd  29928  dvconstbi  30796  2f1fvneq  31733  xihopellsmN  35928  dihopellsm  35929