Theorem anim12dan 627

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  isocnv  7303  isocnv3  7305  f1oiso2  7325  xpexr2  7889  f1o2ndf1  8089  mpof1o2d  8093  fnwelem  8099  omword  8527  oeword  8548  swoso  8701  xpf1o  9100  zorn2lem6  10448  ltapr  10993  ltord1  11703  pc11  16892  imasaddfnlem  17534  imasaddflem  17536  pslem  18580  mgmhmpropd  18708  mhmpropd  18802  frmdsssubm  18871  ghmsub  19240  gasubg  19318  invrpropd  20439  znfld  21585  cygznlem3  21594  mplcoe5lem  22065  evlseu  22109  cpmatmcl  22752  tgclb  23003  innei  23158  txcn  23659  txflf  24039  qustgplem  24154  clmsub4  25141  cfilresi  25330  volcn  25641  itg1addlem4  25734  dvlip  26028  plymullem1  26247  lgsdir2  27364  lgsdchr  27389  brbtwn2  29045  axcontlem7  29110  frgrncvvdeqlem8  30447  nvaddsub4  30799  hhcno  32046  hhcnf  32047  unopf1o  32058  counop  32063  mndlactf1o  33162  mndractf1o  33163  afsval  34925  ontopbas  36736  onsuct0  36749  heicant  38102  ftc1anclem6  38145  equivbnd2  38239  ismtybndlem  38253  ismrer1  38285  iccbnd  38287  ghomco  38338  rngohomco  38421  rngoisocnv  38428  rngoisoco  38429  idlsubcl  38470  xihopellsmN  41826  dihopellsm  41827  dvconstbi  44858  ovolval5lem3  47176  imasetpreimafvbijlemf1  47958  fargshiftf1  47995  upgrimtrlslem2  48475  elpglem1  50280