Theorem anim12dan 625

Description: Conjoin antecedents and consequents in a deduction. (Contributed by Jeff Madsen, 16-Jun-2011.)

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  isocnv  7281  isocnv3  7283  f1oiso2  7303  xpexr2  7866  f1o2ndf1  8068  mpof1o2d  8072  fnwelem  8078  omword  8502  oeword  8523  swoso  8675  xpf1o  9074  zorn2lem6  10421  ltapr  10966  ltord1  11674  pc11  16849  imasaddfnlem  17490  imasaddflem  17492  pslem  18536  mgmhmpropd  18664  mhmpropd  18758  frmdsssubm  18827  ghmsub  19197  gasubg  19275  invrpropd  20396  znfld  21542  cygznlem3  21551  mplcoe5lem  22022  evlseu  22066  cpmatmcl  22709  tgclb  22960  innei  23115  txcn  23616  txflf  23996  qustgplem  24111  clmsub4  25098  cfilresi  25287  volcn  25598  itg1addlem4  25691  dvlip  25985  plymullem1  26204  lgsdir2  27318  lgsdchr  27343  brbtwn2  28999  axcontlem7  29064  frgrncvvdeqlem8  30401  nvaddsub4  30753  hhcno  32000  hhcnf  32001  unopf1o  32012  counop  32017  mndlactf1o  33116  mndractf1o  33117  afsval  34862  ontopbas  36657  onsuct0  36670  heicant  38023  ftc1anclem6  38066  equivbnd2  38160  ismtybndlem  38174  ismrer1  38206  iccbnd  38208  ghomco  38259  rngohomco  38342  rngoisocnv  38349  rngoisoco  38350  idlsubcl  38391  xihopellsmN  41747  dihopellsm  41748  dvconstbi  44779  ovolval5lem3  47098  imasetpreimafvbijlemf1  47880  fargshiftf1  47917  upgrimtrlslem2  48397  elpglem1  50202