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

Theorem anim12dan 812
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 425 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 anim12dan.2 . . . 4  |-  ( (
ph  /\  th )  ->  ta )
43ex 425 . . 3  |-  ( ph  ->  ( th  ->  ta ) )
52, 4anim12d 548 . 2  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
65imp 420 1  |-  ( (
ph  /\  ( ps  /\ 
th ) )  -> 
( ch  /\  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  xpexr2  5310  isocnv  6052  isocnv3  6054  f1oiso2  6074  f1o2ndf1  6456  fnwelem  6463  omword  6815  oeword  6835  swoso  6938  xpf1o  7271  zorn2lem6  8383  ltapr  8924  ltord1  9555  pc11  13255  imasaddfnlem  13755  imasaddflem  13757  pslem  14640  mhmpropd  14746  frmdsssubm  14808  ghmsub  15016  gasubg  15081  invrpropd  15805  znfld  16843  cygznlem3  16852  tgclb  17037  innei  17191  txcn  17660  txflf  18040  divstgplem  18152  cfilresi  19250  volcn  19500  itg1addlem4  19593  dvlip  19879  evlseu  19939  plymullem1  20135  lgsdir2  21114  lgsdchr  21134  fargshiftf1  21626  ghgrplem2  21957  ghsubgolem  21960  vcsub4  22057  nvaddsub4  22144  hhcno  23409  hhcnf  23410  unopf1o  23421  counop  23426  ghomgsg  25106  brbtwn2  25846  axcontlem7  25911  ontopbas  26180  onsuct0  26193  ftc1anclem6  26287  anim12da  26414  equivbnd2  26503  ismtybndlem  26517  ismrer1  26549  iccbnd  26551  dvconstbi  27530  2f1fvneq  28083  usgra2adedgwlkon  28343  frgrancvvdeqlemB  28489  xihopellsmN  32114  dihopellsm  32115
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 179  df-an 362
  Copyright terms: Public domain W3C validator