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

Theorem anim12d 548
Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
Hypotheses
Ref Expression
anim12d.1  |-  ( ph  ->  ( ps  ->  ch ) )
anim12d.2  |-  ( ph  ->  ( th  ->  ta ) )
Assertion
Ref Expression
anim12d  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )

Proof of Theorem anim12d
StepHypRef Expression
1 anim12d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 anim12d.2 . 2  |-  ( ph  ->  ( th  ->  ta ) )
3 idd 23 . 2  |-  ( ph  ->  ( ( ch  /\  ta )  ->  ( ch 
/\  ta ) ) )
41, 2, 3syl2and 471 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  anim1d  549  anim2d  550  prth  556  im2anan9  810  anim12dan  812  3anim123d  1262  2euswap  2359  ssunsn2  3960  disjiun  4205  soss  4524  wess  4572  ordtri3  4620  oneqmini  4635  ordom  4857  frinxp  4946  trin2  5260  xp11  5307  funss  5475  fun  5610  dff13  6007  f1eqcocnv  6031  isores3  6058  isosolem  6070  isowe2  6073  f1oweALT  6077  f1o2ndf1  6457  tposfn2  6504  tposf1o2  6508  smo11  6629  tfrlem1  6639  tz7.48lem  6701  om00  6821  omsmo  6900  ixpfi2  7408  elfiun  7438  supmo  7460  alephord  7961  cardaleph  7975  dfac5  8014  fin1a2lem9  8293  axdc3lem2  8336  zorn2lem6  8386  grudomon  8697  indpi  8789  genpnmax  8889  reclem3pr  8931  reclem4pr  8932  suplem1pr  8934  supsrlem  8991  lemul12b  9872  fimaxre  9960  lbreu  9963  supmullem2  9980  cju  10001  nnind  10023  uz11  10513  xrre2  10763  qbtwnre  10790  xrsupexmnf  10888  xrinfmexpnf  10889  ico0  10967  ioc0  10968  sqrlem6  12058  o1lo1  12336  ruclem9  12842  isprm3  13093  eulerthlem2  13176  prmdiveq  13180  ramub2  13387  lubun  14555  ipodrsima  14596  spwpr4  14668  dirtr  14686  mulgpropd  14928  dprdss  15592  subrgdvds  15887  epttop  17078  cnpresti  17357  cnprest  17358  lmmo  17449  1stcrest  17521  lly1stc  17564  txcnp  17657  addcnlem  18899  caussi  19255  bcthlem5  19286  ovollb2lem  19389  voliunlem1  19449  ioombl1lem4  19460  rolle  19879  c1lip1  19886  c1lip3  19888  ulmval  20301  sqf11  20927  fsumvma  21002  dchrelbas3  21027  constr3trllem2  21643  4cycl4v4e  21658  4cycl4dv  21659  eupai  21694  subgoablo  21904  nmcvcn  22196  sspmval  22237  sspival  22242  sspimsval  22244  sspph  22361  shsubcl  22728  shorth  22802  5oalem6  23166  strlem1  23758  atexch  23889  cdj3i  23949  xrofsup  24131  ishashinf  24164  cnre2csqima  24314  erdszelem9  24890  erdsze2lem2  24895  dedekind  25192  funpsstri  25394  dfon2lem4  25418  dfon2  25424  trpredrec  25521  frmin  25522  wfrlem4  25546  wsuclem  25581  frrlem4  25590  nocvxminlem  25650  nocvxmin  25651  nofulllem5  25666  elfuns  25765  brbtwn2  25849  axeuclidlem  25906  axcontlem9  25916  axcontlem10  25917  btwnswapid  25956  ifscgr  25983  hilbert1.2  26094  supadd  26246  ltflcei  26247  tan2h  26252  mblfinlem3  26257  elicc3  26334  tailfb  26420  fzmul  26458  metf1o  26475  ismtycnv  26525  ismtyres  26531  crngohomfo  26630  prtlem50  26708  pm11.59  27581  infrglb  27712  afvres  28026  swrdnd  28216  swrdvalodmlem1  28221  swrdccatin2  28244  usgra2wlkspthlem2  28345  usgra2adedgspthlem1  28351  usgra2adedgwlkon  28355  usg2wlkonot  28415  usg2wotspth  28416  2pthfrgrarn2  28474  frgranbnb  28484  lubunNEW  29845  hlhgt2  30260  hl2at  30276  2llnjN  30438  2lplnj  30491  linepsubN  30623  cdlemg33b0  31572  dvh3dim3N  32321  mapdh9a  32662
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 179  df-an 362
  Copyright terms: Public domain W3C validator