Theorem anim12dan 630

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  isocnv  7318  isocnv3  7320  f1oiso2  7340  xpexr2  7904  f1o2ndf1  8105  mpof1o2d  8109  fnwelem  8115  omword  8543  oeword  8564  swoso  8717  xpf1o  9115  zorn2lem6  10473  ltapr  11018  ltord1  11728  pc11  16930  imasaddfnlem  17572  imasaddflem  17574  pslem  18618  mgmhmpropd  18746  mhmpropd  18840  frmdsssubm  18910  ghmsub  19285  gasubg  19363  invrpropd  20491  znfld  21670  cygznlem3  21679  mplcoe5lem  22150  evlseu  22194  cpmatmcl  22837  tgclb  23088  innei  23243  txcn  23744  txflf  24124  qustgplem  24239  clmsub4  25226  cfilresi  25415  volcn  25726  itg1addlem4  25819  dvlip  26113  plymullem1  26332  lgsdir2  27452  lgsdchr  27477  brbtwn2  29164  axcontlem7  29229  frgrncvvdeqlem8  30566  nvaddsub4  30918  hhcno  32165  hhcnf  32166  unopf1o  32177  counop  32182  mndlactf1o  33263  mndractf1o  33264  afsval  34978  ontopbas  36801  onsuct0  36814  heicant  38166  ftc1anclem6  38209  equivbnd2  38303  ismtybndlem  38317  ismrer1  38349  iccbnd  38351  ghomco  38402  rngohomco  38485  rngoisocnv  38492  rngoisoco  38493  idlsubcl  38534  xihopellsmN  41890  dihopellsm  41891  dvconstbi  44908  ovolval5lem3  47226  imasetpreimafvbijlemf1  48008  fargshiftf1  48045  upgrimtrlslem2  48525  elpglem1  50340