Theorem anim12dan 900

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 585	. 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 197  df-an 385

This theorem is referenced by:  2f1fvneq  6557  isocnv  6620  isocnv3  6622  f1oiso2  6642  xpexr2  7149  f1o2ndf1  7330  fnwelem  7337  omword  7695  oeword  7715  swoso  7820  xpf1o  8163  zorn2lem6  9361  ltapr  9905  ltord1  10592  pc11  15631  imasaddfnlem  16235  imasaddflem  16237  pslem  17253  mhmpropd  17388  frmdsssubm  17445  ghmsub  17715  gasubg  17781  invrpropd  18744  mplcoe5lem  19515  evlseu  19564  znfld  19957  cygznlem3  19966  cpmatmcl  20572  tgclb  20822  innei  20977  txcn  21477  txflf  21857  qustgplem  21971  clmsub4  22952  cfilresi  23139  volcn  23420  itg1addlem4  23511  dvlip  23801  plymullem1  24015  lgsdir2  25100  lgsdchr  25125  brbtwn2  25830  axcontlem7  25895  frgrncvvdeqlem8  27286  nvaddsub4  27640  hhcno  28891  hhcnf  28892  unopf1o  28903  counop  28908  afsval  30877  ontopbas  32552  onsuct0  32565  heicant  33574  ftc1anclem6  33620  anim12da  33636  equivbnd2  33721  ismtybndlem  33735  ismrer1  33767  iccbnd  33769  xihopellsmN  36860  dihopellsm  36861  dvconstbi  38850  fargshiftf1  41702  mgmhmpropd  42110  elpglem1  42782