Theorem anim12dan 837

Description: Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)

Hypotheses

Ref	Expression
anim12dan.1
anim12dan.2

Assertion

Ref	Expression
anim12dan

Proof of Theorem anim12dan

Step	Hyp	Ref	Expression
1		anim12dan.1	. . . 4
2	1	ex 434	. . 3
3		anim12dan.2	. . . 4
4	3	ex 434	. . 3
5	2, 4	anim12d 563	. 2
6	5	imp 429	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  isocnv  6226  isocnv3  6228  f1oiso2  6248  xpexr2  6741  f1o2ndf1  6908  fnwelem  6915  omword  7238  oeword  7258  swoso  7361  xpf1o  7699  zorn2lem6  8902  ltapr  9444  ltord1  10104  pc11  14403  imasaddfnlem  14925  imasaddflem  14927  pslem  15836  mhmpropd  15972  frmdsssubm  16029  ghmsub  16275  gasubg  16340  invrpropd  17347  mplcoe5lem  18130  evlseu  18185  znfld  18599  cygznlem3  18608  cpmatmcl  19220  tgclb  19472  innei  19626  txcn  20127  txflf  20507  qustgplem  20619  cfilresi  21734  volcn  22015  itg1addlem4  22106  dvlip  22394  plymullem1  22611  lgsdir2  23603  lgsdchr  23623  brbtwn2  24208  axcontlem7  24273  usgra2adedgwlkon  24615  fargshiftf1  24637  frgrancvvdeqlemB  25038  ghgrplem2OLD  25369  ghsubgolemOLD  25372  vcsub4  25469  nvaddsub4  25556  hhcno  26823  hhcnf  26824  unopf1o  26835  counop  26840  afsval  28551  ghomgsg  29033  ontopbas  29893  onsuct0  29906  heicant  30049  ftc1anclem6  30095  anim12da  30201  equivbnd2  30288  ismtybndlem  30302  ismrer1  30334  iccbnd  30336  dvconstbi  31239  2f1fvneq  32307  mgmhmpropd  32473  xihopellsmN  36981  dihopellsm  36982

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