Theorem anim12dan 631

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  isocnv  7334  isocnv3  7336  f1oiso2  7356  xpexr2  7919  f1o2ndf1  8122  mpof1o2d  8126  fnwelem  8132  omword  8560  oeword  8581  swoso  8734  xpf1o  9140  zorn2lem6  10506  ltapr  11057  ltord1  11767  pc11  16976  imasaddfnlem  17618  imasaddflem  17620  pslem  18664  mgmhmpropd  18804  mhmpropd  18904  frmdsssubm  18974  ghmsub  19355  gasubg  19433  invrpropd  20563  znfld  21777  cygznlem3  21786  mplcoe5lem  22259  evlseu  22303  cpmatmcl  22948  tgclb  23199  innei  23354  txcn  23856  txflf  24236  qustgplem  24351  clmsub4  25338  cfilresi  25527  volcn  25838  itg1addlem4  25931  dvlip  26225  plymullem1  26444  lgsdir2  27567  lgsdchr  27592  brbtwn2  29363  axcontlem7  29428  frgrncvvdeqlem8  30787  nvaddsub4  31139  hhcno  32386  hhcnf  32387  unopf1o  32398  counop  32403  mndlactf1o  33472  mndractf1o  33473  afsval  35184  ontopbas  37049  onsuct0  37062  heicant  38406  ftc1anclem6  38449  equivbnd2  38544  ismtybndlem  38558  ismrer1  38590  iccbnd  38592  ghomco  38643  rngohomco  38726  rngoisocnv  38733  rngoisoco  38734  idlsubcl  38775  xihopellsmN  42129  dihopellsm  42130  dvconstbi  45160  ovolval5lem3  47484  imasetpreimafvbijlemf1  48306  fargshiftf1  48343  upgrimtrlslem2  48823  elpglem1  50639