Theorem anim12dan 811

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

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  xpexr2  5267  isocnv  6009  isocnv3  6011  f1oiso2  6031  f1o2ndf1  6413  fnwelem  6420  omword  6772  oeword  6792  swoso  6895  xpf1o  7228  zorn2lem6  8337  ltapr  8878  ltord1  9509  pc11  13208  imasaddfnlem  13708  imasaddflem  13710  pslem  14593  mhmpropd  14699  frmdsssubm  14761  ghmsub  14969  gasubg  15034  invrpropd  15758  znfld  16796  cygznlem3  16805  tgclb  16990  innei  17144  txcn  17611  txflf  17991  divstgplem  18103  cfilresi  19201  volcn  19451  itg1addlem4  19544  dvlip  19830  evlseu  19890  plymullem1  20086  lgsdir2  21065  lgsdchr  21085  fargshiftf1  21577  ghgrplem2  21908  ghsubgolem  21911  vcsub4  22008  nvaddsub4  22095  hhcno  23360  hhcnf  23361  unopf1o  23372  counop  23377  ghomgsg  25057  brbtwn2  25748  axcontlem7  25813  ontopbas  26082  onsuct0  26095  anim12da  26302  equivbnd2  26391  ismtybndlem  26405  ismrer1  26437  iccbnd  26439  dvconstbi  27419  2f1fvneq  27958  usgra2adedgwlkon  28047  frgrancvvdeqlemB  28141  xihopellsmN  31737  dihopellsm  31738

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361