Theorem anim12dan 619

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 609	. 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 207  df-an 396

This theorem is referenced by:  isocnv  7328  isocnv3  7330  f1oiso2  7350  xpexr2  7920  f1o2ndf1  8126  fnwelem  8135  omword  8587  oeword  8607  swoso  8758  xpf1o  9158  zorn2lem6  10520  ltapr  11064  ltord1  11768  pc11  16905  imasaddfnlem  17547  imasaddflem  17549  pslem  18587  mgmhmpropd  18681  mhmpropd  18775  frmdsssubm  18844  ghmsub  19212  gasubg  19290  invrpropd  20383  znfld  21526  cygznlem3  21535  mplcoe5lem  22002  evlseu  22046  cpmatmcl  22662  tgclb  22913  innei  23068  txcn  23569  txflf  23949  qustgplem  24064  clmsub4  25062  cfilresi  25252  volcn  25564  itg1addlem4  25657  dvlip  25955  plymullem1  26176  lgsdir2  27298  lgsdchr  27323  brbtwn2  28889  axcontlem7  28954  frgrncvvdeqlem8  30292  nvaddsub4  30643  hhcno  31890  hhcnf  31891  unopf1o  31902  counop  31907  mndlactf1o  33030  mndractf1o  33031  afsval  34708  ontopbas  36451  onsuct0  36464  heicant  37684  ftc1anclem6  37727  equivbnd2  37821  ismtybndlem  37835  ismrer1  37867  iccbnd  37869  ghomco  37920  rngohomco  38003  rngoisocnv  38010  rngoisoco  38011  idlsubcl  38052  xihopellsmN  41278  dihopellsm  41279  f1o2d2  42251  dvconstbi  44333  ovolval5lem3  46663  imasetpreimafvbijlemf1  47398  fargshiftf1  47435  upgrimtrlslem2  47898  elpglem1  49555