Theorem anim12dan 837

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  6211  isocnv3  6213  f1oiso2  6233  xpexr2  6726  f1o2ndf1  6893  fnwelem  6900  omword  7221  oeword  7241  swoso  7344  xpf1o  7681  zorn2lem6  8884  ltapr  9426  ltord1  10085  pc11  14280  imasaddfnlem  14802  imasaddflem  14804  pslem  15710  mhmpropd  15846  frmdsssubm  15903  ghmsub  16149  gasubg  16214  invrpropd  17221  mplcoe5lem  18004  evlseu  18059  znfld  18472  cygznlem3  18481  cpmatmcl  19093  tgclb  19345  innei  19499  txcn  20000  txflf  20380  qustgplem  20492  cfilresi  21607  volcn  21888  itg1addlem4  21979  dvlip  22267  plymullem1  22484  lgsdir2  23475  lgsdchr  23495  brbtwn2  24080  axcontlem7  24145  usgra2adedgwlkon  24487  fargshiftf1  24509  frgrancvvdeqlemB  24910  ghgrplem2OLD  25241  ghsubgolemOLD  25244  vcsub4  25341  nvaddsub4  25428  hhcno  26695  hhcnf  26696  unopf1o  26707  counop  26712  afsval  28424  ghomgsg  28906  ontopbas  29868  onsuct0  29881  heicant  30024  ftc1anclem6  30070  anim12da  30176  equivbnd2  30263  ismtybndlem  30277  ismrer1  30309  iccbnd  30311  dvconstbi  31215  2f1fvneq  32145  mgmhmpropd  32311  xihopellsmN  36721  dihopellsm  36722