Theorem anim12dan 828

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 560	. 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  6018  isocnv3  6020  f1oiso2  6040  xpexr2  6518  f1o2ndf1  6679  fnwelem  6686  omword  7005  oeword  7025  swoso  7128  xpf1o  7469  zorn2lem6  8666  ltapr  9210  ltord1  9862  pc11  13942  imasaddfnlem  14462  imasaddflem  14464  pslem  15372  mhmpropd  15466  frmdsssubm  15532  ghmsub  15748  gasubg  15813  invrpropd  16780  evlseu  17578  znfld  17952  cygznlem3  17961  tgclb  18534  innei  18688  txcn  19158  txflf  19538  divstgplem  19650  cfilresi  20765  volcn  21045  itg1addlem4  21136  dvlip  21424  plymullem1  21641  lgsdir2  22626  lgsdchr  22646  brbtwn2  23086  axcontlem7  23151  fargshiftf1  23458  ghgrplem2  23789  ghsubgolem  23792  vcsub4  23889  nvaddsub4  23976  hhcno  25243  hhcnf  25244  unopf1o  25255  counop  25260  ghomgsg  27241  ontopbas  28204  onsuct0  28217  heicant  28351  ftc1anclem6  28397  anim12da  28529  equivbnd2  28616  ismtybndlem  28630  ismrer1  28662  iccbnd  28664  dvconstbi  29533  2f1fvneq  30068  usgra2adedgwlkon  30232  frgrancvvdeqlemB  30556  xihopellsmN  34621  dihopellsm  34622