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

Theorem anim12dan 835
Description: Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)
Hypotheses
Ref Expression
anim12dan.1  |-  ( (
ph  /\  ps )  ->  ch )
anim12dan.2  |-  ( (
ph  /\  th )  ->  ta )
Assertion
Ref Expression
anim12dan  |-  ( (
ph  /\  ( ps  /\ 
th ) )  -> 
( ch  /\  ta ) )

Proof of Theorem anim12dan
StepHypRef Expression
1 anim12dan.1 . . . 4  |-  ( (
ph  /\  ps )  ->  ch )
21ex 432 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 anim12dan.2 . . . 4  |-  ( (
ph  /\  th )  ->  ta )
43ex 432 . . 3  |-  ( ph  ->  ( th  ->  ta ) )
52, 4anim12d 561 . 2  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
65imp 427 1  |-  ( (
ph  /\  ( ps  /\ 
th ) )  -> 
( ch  /\  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  isocnv  6201  isocnv3  6203  f1oiso2  6223  xpexr2  6714  f1o2ndf1  6881  fnwelem  6888  omword  7211  oeword  7231  swoso  7334  xpf1o  7672  zorn2lem6  8872  ltapr  9412  ltord1  10075  pc11  14487  imasaddfnlem  15017  imasaddflem  15019  pslem  16035  mhmpropd  16171  frmdsssubm  16228  ghmsub  16474  gasubg  16539  invrpropd  17542  mplcoe5lem  18325  evlseu  18380  znfld  18772  cygznlem3  18781  cpmatmcl  19387  tgclb  19639  innei  19793  txcn  20293  txflf  20673  qustgplem  20785  cfilresi  21900  volcn  22181  itg1addlem4  22272  dvlip  22560  plymullem1  22777  lgsdir2  23801  lgsdchr  23821  brbtwn2  24410  axcontlem7  24475  usgra2adedgwlkon  24817  fargshiftf1  24839  frgrancvvdeqlemB  25240  ghgrplem2OLD  25567  ghsubgolemOLD  25570  vcsub4  25667  nvaddsub4  25754  hhcno  27021  hhcnf  27022  unopf1o  27033  counop  27038  afsval  28815  ghomgsg  29297  ontopbas  30121  onsuct0  30134  heicant  30289  ftc1anclem6  30335  anim12da  30441  equivbnd2  30528  ismtybndlem  30542  ismrer1  30574  iccbnd  30576  dvconstbi  31480  2f1fvneq  32681  mgmhmpropd  32845  xihopellsmN  37378  dihopellsm  37379
  Copyright terms: Public domain W3C validator