Theorem anim12dan 618

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

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  2f1fvneq  7127  isocnv  7194  isocnv3  7196  f1oiso2  7216  xpexr2  7753  f1o2ndf1  7947  fnwelem  7956  omword  8377  oeword  8397  swoso  8505  xpf1o  8891  zorn2lem6  10241  ltapr  10785  ltord1  11484  pc11  16562  imasaddfnlem  17220  imasaddflem  17222  pslem  18271  mhmpropd  18417  frmdsssubm  18481  ghmsub  18823  gasubg  18889  invrpropd  19921  znfld  20749  cygznlem3  20758  mplcoe5lem  21221  evlseu  21274  cpmatmcl  21849  tgclb  22101  innei  22257  txcn  22758  txflf  23138  qustgplem  23253  clmsub4  24250  cfilresi  24440  volcn  24751  itg1addlem4  24844  itg1addlem4OLD  24845  dvlip  25138  plymullem1  25356  lgsdir2  26459  lgsdchr  26484  brbtwn2  27254  axcontlem7  27319  frgrncvvdeqlem8  28649  nvaddsub4  28998  hhcno  30245  hhcnf  30246  unopf1o  30257  counop  30262  afsval  32630  ontopbas  34596  onsuct0  34609  heicant  35791  ftc1anclem6  35834  equivbnd2  35929  ismtybndlem  35943  ismrer1  35975  iccbnd  35977  ghomco  36028  rngohomco  36111  rngoisocnv  36118  rngoisoco  36119  idlsubcl  36160  xihopellsmN  39247  dihopellsm  39248  mhphf  40265  dvconstbi  41905  imasetpreimafvbijlemf1  44808  fargshiftf1  44845  mgmhmpropd  45291  elpglem1  46368