Theorem anim12dan 833

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  6120  isocnv3  6122  f1oiso2  6142  xpexr2  6619  f1o2ndf1  6780  fnwelem  6787  omword  7109  oeword  7129  swoso  7232  xpf1o  7573  zorn2lem6  8771  ltapr  9315  ltord1  9967  pc11  14048  imasaddfnlem  14568  imasaddflem  14570  pslem  15478  mhmpropd  15572  frmdsssubm  15641  ghmsub  15857  gasubg  15922  invrpropd  16896  mplcoe5lem  17654  evlseu  17709  znfld  18102  cygznlem3  18111  tgclb  18691  innei  18845  txcn  19315  txflf  19695  divstgplem  19807  cfilresi  20922  volcn  21202  itg1addlem4  21293  dvlip  21581  plymullem1  21798  lgsdir2  22783  lgsdchr  22803  brbtwn2  23286  axcontlem7  23351  fargshiftf1  23658  ghgrplem2  23989  ghsubgolem  23992  vcsub4  24089  nvaddsub4  24176  hhcno  25443  hhcnf  25444  unopf1o  25455  counop  25460  ghomgsg  27446  ontopbas  28408  onsuct0  28421  heicant  28564  ftc1anclem6  28610  anim12da  28742  equivbnd2  28829  ismtybndlem  28843  ismrer1  28875  iccbnd  28877  dvconstbi  29746  2f1fvneq  30281  usgra2adedgwlkon  30445  frgrancvvdeqlemB  30769  cpmatmcl  31182  xihopellsmN  35205  dihopellsm  35206