Theorem anim12dan 845

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

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  isocnv  6233  isocnv3  6235  f1oiso2  6255  xpexr2  6745  f1o2ndf1  6912  fnwelem  6919  omword  7276  oeword  7296  swoso  7399  xpf1o  7737  zorn2lem6  8932  ltapr  9471  ltord1  10141  pc11  14817  imasaddfnlem  15422  imasaddflem  15424  pslem  16440  mhmpropd  16576  frmdsssubm  16633  ghmsub  16879  gasubg  16944  invrpropd  17914  mplcoe5lem  18679  evlseu  18727  znfld  19118  cygznlem3  19127  cpmatmcl  19730  tgclb  19973  innei  20128  txcn  20628  txflf  21008  qustgplem  21122  cfilresi  22252  volcn  22551  itg1addlem4  22644  dvlip  22932  plymullem1  23155  lgsdir2  24243  lgsdchr  24263  brbtwn2  24922  axcontlem7  24987  usgra2adedgwlkon  25329  fargshiftf1  25351  frgrancvvdeqlemB  25752  ghgrplem2OLD  26081  ghsubgolemOLD  26084  vcsub4  26181  nvaddsub4  26268  hhcno  27543  hhcnf  27544  unopf1o  27555  counop  27560  afsval  29484  ghomgsg  30307  ontopbas  31081  onsuct0  31094  heicant  31889  ftc1anclem6  31936  anim12da  31952  equivbnd2  32038  ismtybndlem  32052  ismrer1  32084  iccbnd  32086  xihopellsmN  34741  dihopellsm  34742  dvconstbi  36541  2f1fvneq  38713  mgmhmpropd  39057