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:  2f1fvneq  7280  isocnv  7350  isocnv3  7352  f1oiso2  7372  xpexr2  7942  f1o2ndf1  8146  fnwelem  8155  omword  8607  oeword  8627  swoso  8778  xpf1o  9178  zorn2lem6  10539  ltapr  11083  ltord1  11787  pc11  16914  imasaddfnlem  17575  imasaddflem  17577  pslem  18630  mgmhmpropd  18724  mhmpropd  18818  frmdsssubm  18887  ghmsub  19255  gasubg  19333  invrpropd  20435  znfld  21597  cygznlem3  21606  mplcoe5lem  22075  evlseu  22125  cpmatmcl  22741  tgclb  22993  innei  23149  txcn  23650  txflf  24030  qustgplem  24145  clmsub4  25153  cfilresi  25343  volcn  25655  itg1addlem4  25748  itg1addlem4OLD  25749  dvlip  26047  plymullem1  26268  lgsdir2  27389  lgsdchr  27414  brbtwn2  28935  axcontlem7  29000  frgrncvvdeqlem8  30335  nvaddsub4  30686  hhcno  31933  hhcnf  31934  unopf1o  31945  counop  31950  mndlactf1o  33018  mndractf1o  33019  afsval  34665  ontopbas  36411  onsuct0  36424  heicant  37642  ftc1anclem6  37685  equivbnd2  37779  ismtybndlem  37793  ismrer1  37825  iccbnd  37827  ghomco  37878  rngohomco  37961  rngoisocnv  37968  rngoisoco  37969  idlsubcl  38010  xihopellsmN  41237  dihopellsm  41238  f1o2d2  42253  dvconstbi  44330  ovolval5lem3  46610  imasetpreimafvbijlemf1  47329  fargshiftf1  47366  elpglem1  48942