MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anim12dan Structured version   Visualization version   GIF version

Theorem anim12dan 618
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
StepHypRef Expression
1 anim12dan.1 . . . 4 ((𝜑𝜓) → 𝜒)
21ex 413 . . 3 (𝜑 → (𝜓𝜒))
3 anim12dan.2 . . . 4 ((𝜑𝜃) → 𝜏)
43ex 413 . . 3 (𝜑 → (𝜃𝜏))
52, 4anim12d 608 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
65imp 407 1 ((𝜑 ∧ (𝜓𝜃)) → (𝜒𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  2f1fvneq  7009  isocnv  7072  isocnv3  7074  f1oiso2  7094  xpexr2  7613  f1o2ndf1  7807  fnwelem  7814  omword  8185  oeword  8205  swoso  8311  xpf1o  8667  zorn2lem6  9911  ltapr  10455  ltord1  11154  pc11  16204  imasaddfnlem  16789  imasaddflem  16791  pslem  17804  mhmpropd  17950  frmdsssubm  18014  ghmsub  18304  gasubg  18370  invrpropd  19377  mplcoe5lem  20176  evlseu  20224  znfld  20635  cygznlem3  20644  cpmatmcl  21255  tgclb  21506  innei  21661  txcn  22162  txflf  22542  qustgplem  22656  clmsub4  23637  cfilresi  23825  volcn  24134  itg1addlem4  24227  dvlip  24517  plymullem1  24731  lgsdir2  25833  lgsdchr  25858  brbtwn2  26618  axcontlem7  26683  frgrncvvdeqlem8  28012  nvaddsub4  28361  hhcno  29608  hhcnf  29609  unopf1o  29620  counop  29625  afsval  31841  ontopbas  33673  onsuct0  33686  heicant  34808  ftc1anclem6  34853  equivbnd2  34951  ismtybndlem  34965  ismrer1  34997  iccbnd  34999  ghomco  35050  rngohomco  35133  rngoisocnv  35140  rngoisoco  35141  idlsubcl  35182  xihopellsmN  38270  dihopellsm  38271  dvconstbi  40543  imasetpreimafvbijlemf1  43441  fargshiftf1  43478  mgmhmpropd  43929  elpglem1  44741
  Copyright terms: Public domain W3C validator