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  5131  isocnv  5843  isocnv3  5845  f1oiso2  5865  fnwelem  6246  omword  6584  oeword  6604  swoso  6707  xpf1o  7039  zorn2lem6  8144  ltapr  8685  ltord1  9315  pc11  12948  imasaddfnlem  13446  imasaddflem  13448  pslem  14331  mhmpropd  14437  frmdsssubm  14499  ghmsub  14707  gasubg  14772  invrpropd  15496  znfld  16530  cygznlem3  16539  tgclb  16724  innei  16878  txcn  17336  txflf  17717  divstgplem  17819  cfilresi  18737  volcn  18977  itg1addlem4  19070  dvlip  19356  evlseu  19416  plymullem1  19612  lgsdir2  20583  lgsdchr  20603  ghgrplem2  21050  ghsubgolem  21053  vcsub4  21148  nvaddsub4  21235  hhcno  22500  hhcnf  22501  unopf1o  22512  counop  22517  ghomgsg  24015  brbtwn2  24605  axcontlem7  24670  ontopbas  24939  onsuct0  24952  fprodsub  25482  invaddvec  25570  cmp2morpcatt  26065  anim12da  26435  equivbnd2  26619  ismtybndlem  26633  ismrer1  26665  iccbnd  26667  dvconstbi  27654  fargshiftf1  28382  xihopellsmN  32066  dihopellsm  32067
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