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

Theorem anim12dan 621
 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 416 . . 3 (𝜑 → (𝜓𝜒))
3 anim12dan.2 . . . 4 ((𝜑𝜃) → 𝜏)
43ex 416 . . 3 (𝜑 → (𝜃𝜏))
52, 4anim12d 611 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
65imp 410 1 ((𝜑 ∧ (𝜓𝜃)) → (𝜒𝜏))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 400 This theorem is referenced by:  2f1fvneq  7001  isocnv  7067  isocnv3  7069  f1oiso2  7089  xpexr2  7613  f1o2ndf1  7808  fnwelem  7815  omword  8186  oeword  8206  swoso  8312  xpf1o  8670  zorn2lem6  9919  ltapr  10463  ltord1  11162  pc11  16213  imasaddfnlem  16800  imasaddflem  16802  pslem  17815  mhmpropd  17961  frmdsssubm  18025  ghmsub  18366  gasubg  18432  invrpropd  19452  znfld  20261  cygznlem3  20270  mplcoe5lem  20719  evlseu  20765  cpmatmcl  21338  tgclb  21589  innei  21744  txcn  22245  txflf  22625  qustgplem  22740  clmsub4  23725  cfilresi  23913  volcn  24224  itg1addlem4  24317  dvlip  24610  plymullem1  24825  lgsdir2  25928  lgsdchr  25953  brbtwn2  26713  axcontlem7  26778  frgrncvvdeqlem8  28105  nvaddsub4  28454  hhcno  29701  hhcnf  29702  unopf1o  29713  counop  29718  afsval  32088  ontopbas  33925  onsuct0  33938  heicant  35132  ftc1anclem6  35175  equivbnd2  35270  ismtybndlem  35284  ismrer1  35316  iccbnd  35318  ghomco  35369  rngohomco  35452  rngoisocnv  35459  rngoisoco  35460  idlsubcl  35501  xihopellsmN  38590  dihopellsm  38591  mhphf  39523  dvconstbi  41102  imasetpreimafvbijlemf1  43982  fargshiftf1  44019  mgmhmpropd  44466  elpglem1  45299
 Copyright terms: Public domain W3C validator