Theorem anim12dan 918

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 587	. 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  6680  isocnv  6743  isocnv3  6745  f1oiso2  6765  xpexr2  7272  f1o2ndf1  7453  fnwelem  7460  omword  7819  oeword  7839  swoso  7944  xpf1o  8287  zorn2lem6  9515  ltapr  10059  ltord1  10746  pc11  15786  imasaddfnlem  16390  imasaddflem  16392  pslem  17407  mhmpropd  17542  frmdsssubm  17599  ghmsub  17869  gasubg  17935  invrpropd  18898  mplcoe5lem  19669  evlseu  19718  znfld  20111  cygznlem3  20120  cpmatmcl  20726  tgclb  20976  innei  21131  txcn  21631  txflf  22011  qustgplem  22125  clmsub4  23106  cfilresi  23293  volcn  23574  itg1addlem4  23665  dvlip  23955  plymullem1  24169  lgsdir2  25254  lgsdchr  25279  brbtwn2  25984  axcontlem7  26049  frgrncvvdeqlem8  27460  nvaddsub4  27821  hhcno  29072  hhcnf  29073  unopf1o  29084  counop  29089  afsval  31058  ontopbas  32733  onsuct0  32746  heicant  33757  ftc1anclem6  33803  anim12da  33819  equivbnd2  33904  ismtybndlem  33918  ismrer1  33950  iccbnd  33952  xihopellsmN  37045  dihopellsm  37046  dvconstbi  39035  fargshiftf1  41887  mgmhmpropd  42295  elpglem1  42967