Theorem anim12dan 613

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

Syntax hints:   → wi 4   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  2f1fvneq  6745  isocnv  6808  isocnv3  6810  f1oiso2  6830  xpexr2  7342  f1o2ndf1  7522  fnwelem  7529  omword  7890  oeword  7910  swoso  8015  xpf1o  8364  zorn2lem6  9611  ltapr  10155  ltord1  10846  pc11  15917  imasaddfnlem  16503  imasaddflem  16505  pslem  17521  mhmpropd  17656  frmdsssubm  17714  ghmsub  17981  gasubg  18047  invrpropd  19014  mplcoe5lem  19790  evlseu  19838  znfld  20230  cygznlem3  20239  cpmatmcl  20852  tgclb  21103  innei  21258  txcn  21758  txflf  22138  qustgplem  22252  clmsub4  23233  cfilresi  23421  volcn  23714  itg1addlem4  23807  dvlip  24097  plymullem1  24311  lgsdir2  25407  lgsdchr  25432  brbtwn2  26142  axcontlem7  26207  frgrncvvdeqlem8  27655  nvaddsub4  28037  hhcno  29288  hhcnf  29289  unopf1o  29300  counop  29305  afsval  31269  ontopbas  32935  onsuct0  32948  heicant  33933  ftc1anclem6  33978  anim12da  33994  equivbnd2  34078  ismtybndlem  34092  ismrer1  34124  iccbnd  34126  xihopellsmN  37275  dihopellsm  37276  dvconstbi  39315  fargshiftf1  42217  mgmhmpropd  42584  elpglem1  43256