Theorem anim12dan 620

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 610	. 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  7276  isocnv3  7278  f1oiso2  7298  xpexr2  7861  f1o2ndf1  8063  fnwelem  8072  omword  8496  oeword  8517  swoso  8669  xpf1o  9068  zorn2lem6  10412  ltapr  10957  ltord1  11665  pc11  16840  imasaddfnlem  17481  imasaddflem  17483  pslem  18527  mgmhmpropd  18655  mhmpropd  18749  frmdsssubm  18818  ghmsub  19188  gasubg  19266  invrpropd  20387  znfld  21548  cygznlem3  21557  mplcoe5lem  22026  evlseu  22070  cpmatmcl  22693  tgclb  22944  innei  23099  txcn  23600  txflf  23980  qustgplem  24095  clmsub4  25082  cfilresi  25271  volcn  25582  itg1addlem4  25675  dvlip  25970  plymullem1  26191  lgsdir2  27312  lgsdchr  27337  brbtwn2  28993  axcontlem7  29058  frgrncvvdeqlem8  30396  nvaddsub4  30748  hhcno  31995  hhcnf  31996  unopf1o  32007  counop  32012  mndlactf1o  33110  mndractf1o  33111  afsval  34836  ontopbas  36631  onsuct0  36644  heicant  37987  ftc1anclem6  38030  equivbnd2  38124  ismtybndlem  38138  ismrer1  38170  iccbnd  38172  ghomco  38223  rngohomco  38306  rngoisocnv  38313  rngoisoco  38314  idlsubcl  38355  xihopellsmN  41711  dihopellsm  41712  f1o2d2  42685  dvconstbi  44776  ovolval5lem3  47097  imasetpreimafvbijlemf1  47861  fargshiftf1  47898  upgrimtrlslem2  48378  elpglem1  50183