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

Theorem anim12dan 878
 Description: Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)
Hypotheses
Ref Expression
anim12dan.1 ((𝜑𝜓) → 𝜒)
anim12dan.2 ((𝜑𝜃) → 𝜏)
Assertion
Ref Expression
anim12dan ((𝜑 ∧ (𝜓𝜃)) → (𝜒𝜏))

Proof of Theorem anim12dan
StepHypRef Expression
1 anim12dan.1 . . . 4 ((𝜑𝜓) → 𝜒)
21ex 449 . . 3 (𝜑 → (𝜓𝜒))
3 anim12dan.2 . . . 4 ((𝜑𝜃) → 𝜏)
43ex 449 . . 3 (𝜑 → (𝜃𝜏))
52, 4anim12d 584 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
65imp 444 1 ((𝜑 ∧ (𝜓𝜃)) → (𝜒𝜏))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  isocnv  6480  isocnv3  6482  f1oiso2  6502  xpexr2  7000  f1o2ndf1  7172  fnwelem  7179  omword  7537  oeword  7557  swoso  7662  xpf1o  8007  zorn2lem6  9206  ltapr  9746  ltord1  10433  pc11  15422  imasaddfnlem  16011  imasaddflem  16013  pslem  17029  mhmpropd  17164  frmdsssubm  17221  ghmsub  17491  gasubg  17558  invrpropd  18521  mplcoe5lem  19288  evlseu  19337  znfld  19728  cygznlem3  19737  cpmatmcl  20343  tgclb  20585  innei  20739  txcn  21239  txflf  21620  qustgplem  21734  clmsub4  22714  cfilresi  22901  volcn  23180  itg1addlem4  23272  dvlip  23560  plymullem1  23774  lgsdir2  24855  lgsdchr  24880  brbtwn2  25585  axcontlem7  25650  usgra2adedgwlkon  26143  fargshiftf1  26165  frgrancvvdeqlemB  26565  nvaddsub4  26896  hhcno  28147  hhcnf  28148  unopf1o  28159  counop  28164  afsval  30002  ontopbas  31597  onsuct0  31610  heicant  32614  ftc1anclem6  32660  anim12da  32676  equivbnd2  32761  ismtybndlem  32775  ismrer1  32807  iccbnd  32809  xihopellsmN  35561  dihopellsm  35562  dvconstbi  37555  2f1fvneq  40322  frgrncvvdeqlemB  41477  mgmhmpropd  41575  elpglem1  42253
 Copyright terms: Public domain W3C validator