Theorem anim12dan 878

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  isocnv  6480  isocnv3  6482  f1oiso2  6502  xpexr2  7000  f1o2ndf1  7172  fnwelem  7179  omword  7537  oeword  7557  swoso  7662  xpf1o  8007  zorn2lem6  9206  ltapr  9746  ltord1  10433  pc11  15422  imasaddfnlem  16011  imasaddflem  16013  pslem  17029  mhmpropd  17164  frmdsssubm  17221  ghmsub  17491  gasubg  17558  invrpropd  18521  mplcoe5lem  19288  evlseu  19337  znfld  19728  cygznlem3  19737  cpmatmcl  20343  tgclb  20585  innei  20739  txcn  21239  txflf  21620  qustgplem  21734  clmsub4  22714  cfilresi  22901  volcn  23180  itg1addlem4  23272  dvlip  23560  plymullem1  23774  lgsdir2  24855  lgsdchr  24880  brbtwn2  25585  axcontlem7  25650  usgra2adedgwlkon  26143  fargshiftf1  26165  frgrancvvdeqlemB  26565  nvaddsub4  26896  hhcno  28147  hhcnf  28148  unopf1o  28159  counop  28164  afsval  30002  ontopbas  31597  onsuct0  31610  heicant  32614  ftc1anclem6  32660  anim12da  32676  equivbnd2  32761  ismtybndlem  32775  ismrer1  32807  iccbnd  32809  xihopellsmN  35561  dihopellsm  35562  dvconstbi  37555  2f1fvneq  40322  frgrncvvdeqlemB  41477  mgmhmpropd  41575  elpglem1  42253