Theorem anim12dan 877

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 448	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		anim12dan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
4	3	ex 448	. . 3 ⊢ (𝜑 → (𝜃 → 𝜏))
5	2, 4	anim12d 583	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))
6	5	imp 443	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏))

Syntax hints:   → wi 4   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  isocnv  6458  isocnv3  6460  f1oiso2  6480  xpexr2  6978  f1o2ndf1  7150  fnwelem  7157  omword  7515  oeword  7535  swoso  7640  xpf1o  7985  zorn2lem6  9184  ltapr  9724  ltord1  10406  pc11  15371  imasaddfnlem  15960  imasaddflem  15962  pslem  16978  mhmpropd  17113  frmdsssubm  17170  ghmsub  17440  gasubg  17507  invrpropd  18470  mplcoe5lem  19237  evlseu  19286  znfld  19676  cygznlem3  19685  cpmatmcl  20291  tgclb  20533  innei  20687  txcn  21187  txflf  21568  qustgplem  21682  clmsub4  22662  cfilresi  22846  volcn  23125  itg1addlem4  23217  dvlip  23505  plymullem1  23719  lgsdir2  24800  lgsdchr  24825  brbtwn2  25531  axcontlem7  25596  usgra2adedgwlkon  25937  fargshiftf1  25959  frgrancvvdeqlemB  26359  vcsub4OLD  26625  nvaddsub4  26714  hhcno  27981  hhcnf  27982  unopf1o  27993  counop  27998  afsval  29836  ontopbas  31431  onsuct0  31444  heicant  32438  ftc1anclem6  32484  anim12da  32500  equivbnd2  32585  ismtybndlem  32599  ismrer1  32631  iccbnd  32633  xihopellsmN  35385  dihopellsm  35386  dvconstbi  37379  2f1fvneq  40158  frgrncvvdeqlemB  41499  mgmhmpropd  41597