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

Theorem anim12dan 810
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 423 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 anim12dan.2 . . . 4  |-  ( (
ph  /\  th )  ->  ta )
43ex 423 . . 3  |-  ( ph  ->  ( th  ->  ta ) )
52, 4anim12d 546 . 2  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
65imp 418 1  |-  ( (
ph  /\  ( ps  /\ 
th ) )  -> 
( ch  /\  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  xpexr2  5115  isocnv  5827  isocnv3  5829  f1oiso2  5849  fnwelem  6230  omword  6568  oeword  6588  swoso  6691  xpf1o  7023  zorn2lem6  8128  ltapr  8669  ltord1  9299  pc11  12932  imasaddfnlem  13430  imasaddflem  13432  pslem  14315  mhmpropd  14421  frmdsssubm  14483  ghmsub  14691  gasubg  14756  invrpropd  15480  znfld  16514  cygznlem3  16523  tgclb  16708  innei  16862  txcn  17320  txflf  17701  divstgplem  17803  cfilresi  18721  volcn  18961  itg1addlem4  19054  dvlip  19340  evlseu  19400  plymullem1  19596  lgsdir2  20567  lgsdchr  20587  ghgrplem2  21034  ghsubgolem  21037  vcsub4  21132  nvaddsub4  21219  hhcno  22484  hhcnf  22485  unopf1o  22496  counop  22501  ghomgsg  24000  brbtwn2  24533  axcontlem7  24598  ontopbas  24867  onsuct0  24880  fprodsub  25379  invaddvec  25467  cmp2morpcatt  25962  anim12da  26332  equivbnd2  26516  ismtybndlem  26530  ismrer1  26562  iccbnd  26564  dvconstbi  27551  xihopellsmN  31444  dihopellsm  31445
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator