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  7328  isocnv3  7330  f1oiso2  7350  xpexr2  7915  f1o2ndf1  8116  mpof1o2d  8120  fnwelem  8126  omword  8554  oeword  8575  swoso  8728  xpf1o  9126  zorn2lem6  10484  ltapr  11029  ltord1  11739  pc11  16939  imasaddfnlem  17581  imasaddflem  17583  pslem  18627  mgmhmpropd  18755  mhmpropd  18849  frmdsssubm  18919  ghmsub  19293  gasubg  19371  invrpropd  20499  znfld  21689  cygznlem3  21698  mplcoe5lem  22169  evlseu  22213  cpmatmcl  22855  tgclb  23106  innei  23261  txcn  23762  txflf  24142  qustgplem  24257  clmsub4  25244  cfilresi  25433  volcn  25744  itg1addlem4  25837  dvlip  26131  plymullem1  26350  lgsdir2  27470  lgsdchr  27495  brbtwn2  29221  axcontlem7  29286  frgrncvvdeqlem8  30623  nvaddsub4  30975  hhcno  32222  hhcnf  32223  unopf1o  32234  counop  32239  mndlactf1o  33316  mndractf1o  33317  afsval  35027  ontopbas  36905  onsuct0  36918  heicant  38272  ftc1anclem6  38315  equivbnd2  38409  ismtybndlem  38423  ismrer1  38455  iccbnd  38457  ghomco  38508  rngohomco  38591  rngoisocnv  38598  rngoisoco  38599  idlsubcl  38640  xihopellsmN  41996  dihopellsm  41997  dvconstbi  45014  ovolval5lem3  47338  imasetpreimafvbijlemf1  48120  fargshiftf1  48157  upgrimtrlslem2  48637  elpglem1  50456