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

Theorem anim12dan 877
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 448 . . 3 (𝜑 → (𝜓𝜒))
3 anim12dan.2 . . . 4 ((𝜑𝜃) → 𝜏)
43ex 448 . . 3 (𝜑 → (𝜃𝜏))
52, 4anim12d 583 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
65imp 443 1 ((𝜑 ∧ (𝜓𝜃)) → (𝜒𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  isocnv  6458  isocnv3  6460  f1oiso2  6480  xpexr2  6978  f1o2ndf1  7150  fnwelem  7157  omword  7515  oeword  7535  swoso  7640  xpf1o  7985  zorn2lem6  9184  ltapr  9724  ltord1  10406  pc11  15371  imasaddfnlem  15960  imasaddflem  15962  pslem  16978  mhmpropd  17113  frmdsssubm  17170  ghmsub  17440  gasubg  17507  invrpropd  18470  mplcoe5lem  19237  evlseu  19286  znfld  19676  cygznlem3  19685  cpmatmcl  20291  tgclb  20533  innei  20687  txcn  21187  txflf  21568  qustgplem  21682  clmsub4  22662  cfilresi  22846  volcn  23125  itg1addlem4  23217  dvlip  23505  plymullem1  23719  lgsdir2  24800  lgsdchr  24825  brbtwn2  25531  axcontlem7  25596  usgra2adedgwlkon  25937  fargshiftf1  25959  frgrancvvdeqlemB  26359  vcsub4OLD  26625  nvaddsub4  26714  hhcno  27981  hhcnf  27982  unopf1o  27993  counop  27998  afsval  29836  ontopbas  31431  onsuct0  31444  heicant  32438  ftc1anclem6  32484  anim12da  32500  equivbnd2  32585  ismtybndlem  32599  ismrer1  32631  iccbnd  32633  xihopellsmN  35385  dihopellsm  35386  dvconstbi  37379  2f1fvneq  40158  frgrncvvdeqlemB  41499  mgmhmpropd  41597
  Copyright terms: Public domain W3C validator