Theorem anim12dan 853

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  isocnv  6246  isocnv3  6248  f1oiso2  6268  xpexr2  6761  f1o2ndf1  6931  fnwelem  6938  omword  7297  oeword  7317  swoso  7420  xpf1o  7760  zorn2lem6  8957  ltapr  9496  ltord1  10168  pc11  14878  imasaddfnlem  15483  imasaddflem  15485  pslem  16501  mhmpropd  16637  frmdsssubm  16694  ghmsub  16940  gasubg  17005  invrpropd  17975  mplcoe5lem  18740  evlseu  18788  znfld  19180  cygznlem3  19189  cpmatmcl  19792  tgclb  20035  innei  20190  txcn  20690  txflf  21070  qustgplem  21184  cfilresi  22314  volcn  22613  itg1addlem4  22706  dvlip  22994  plymullem1  23217  lgsdir2  24305  lgsdchr  24325  brbtwn2  24984  axcontlem7  25049  usgra2adedgwlkon  25392  fargshiftf1  25414  frgrancvvdeqlemB  25815  ghgrplem2OLD  26144  ghsubgolemOLD  26147  vcsub4  26244  nvaddsub4  26331  hhcno  27606  hhcnf  27607  unopf1o  27618  counop  27623  afsval  29537  ghomgsg  30360  ontopbas  31137  onsuct0  31150  heicant  32020  ftc1anclem6  32067  anim12da  32083  equivbnd2  32169  ismtybndlem  32183  ismrer1  32215  iccbnd  32217  xihopellsmN  34867  dihopellsm  34868  dvconstbi  36727  2f1fvneq  39054  mgmhmpropd  40058