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:  isocnv  7271  isocnv3  7273  f1oiso2  7293  xpexr2  7859  f1o2ndf1  8062  fnwelem  8071  omword  8495  oeword  8515  swoso  8666  xpf1o  9063  zorn2lem6  10414  ltapr  10958  ltord1  11664  pc11  16810  imasaddfnlem  17450  imasaddflem  17452  pslem  18496  mgmhmpropd  18590  mhmpropd  18684  frmdsssubm  18753  ghmsub  19121  gasubg  19199  invrpropd  20321  znfld  21485  cygznlem3  21494  mplcoe5lem  21962  evlseu  22006  cpmatmcl  22622  tgclb  22873  innei  23028  txcn  23529  txflf  23909  qustgplem  24024  clmsub4  25022  cfilresi  25211  volcn  25523  itg1addlem4  25616  dvlip  25914  plymullem1  26135  lgsdir2  27257  lgsdchr  27282  brbtwn2  28868  axcontlem7  28933  frgrncvvdeqlem8  30268  nvaddsub4  30619  hhcno  31866  hhcnf  31867  unopf1o  31878  counop  31883  mndlactf1o  32997  mndractf1o  32998  afsval  34638  ontopbas  36401  onsuct0  36414  heicant  37634  ftc1anclem6  37677  equivbnd2  37771  ismtybndlem  37785  ismrer1  37817  iccbnd  37819  ghomco  37870  rngohomco  37953  rngoisocnv  37960  rngoisoco  37961  idlsubcl  38002  xihopellsmN  41233  dihopellsm  41234  f1o2d2  42206  dvconstbi  44307  ovolval5lem3  46636  imasetpreimafvbijlemf1  47389  fargshiftf1  47426  upgrimtrlslem2  47889  elpglem1  49684