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

Theorem anim12d 547
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 22 . 2  |-  ( ph  ->  ( ( ch  /\  ta )  ->  ( ch 
/\  ta ) ) )
41, 2, 3syl2and 470 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  anim1d  548  anim2d  549  prth  555  im2anan9  809  anim12dan  811  3anim123d  1261  2euswap  2356  ssunsn2  3950  disjiun  4194  soss  4513  wess  4561  ordtri3  4609  oneqmini  4624  ordom  4846  frinxp  4935  trin2  5249  xp11  5296  funss  5464  fun  5599  dff13  5996  f1eqcocnv  6020  isores3  6047  isosolem  6059  isowe2  6062  f1oweALT  6066  f1o2ndf1  6446  tposfn2  6493  tposf1o2  6497  smo11  6618  tfrlem1  6628  tz7.48lem  6690  om00  6810  omsmo  6889  ixpfi2  7397  elfiun  7427  supmo  7449  alephord  7948  cardaleph  7962  dfac5  8001  fin1a2lem9  8280  axdc3lem2  8323  zorn2lem6  8373  grudomon  8684  indpi  8776  genpnmax  8876  reclem3pr  8918  reclem4pr  8919  suplem1pr  8921  supsrlem  8978  lemul12b  9859  fimaxre  9947  lbreu  9950  supmullem2  9967  cju  9988  nnind  10010  uz11  10500  xrre2  10750  qbtwnre  10777  xrsupexmnf  10875  xrinfmexpnf  10876  ico0  10954  ioc0  10955  sqrlem6  12045  o1lo1  12323  ruclem9  12829  isprm3  13080  eulerthlem2  13163  prmdiveq  13167  ramub2  13374  lubun  14542  ipodrsima  14583  spwpr4  14655  dirtr  14673  mulgpropd  14915  dprdss  15579  subrgdvds  15874  epttop  17065  cnpresti  17344  cnprest  17345  lmmo  17436  1stcrest  17508  lly1stc  17551  txcnp  17644  addcnlem  18886  caussi  19242  bcthlem5  19273  ovollb2lem  19376  voliunlem1  19436  ioombl1lem4  19447  rolle  19866  c1lip1  19873  c1lip3  19875  ulmval  20288  sqf11  20914  fsumvma  20989  dchrelbas3  21014  constr3trllem2  21630  4cycl4v4e  21645  4cycl4dv  21646  eupai  21681  subgoablo  21891  nmcvcn  22183  sspmval  22224  sspival  22229  sspimsval  22231  sspph  22348  shsubcl  22715  shorth  22789  5oalem6  23153  strlem1  23745  atexch  23876  cdj3i  23936  xrofsup  24118  ishashinf  24151  cnre2csqima  24301  erdszelem9  24877  erdsze2lem2  24882  dedekind  25179  funpsstri  25381  dfon2lem4  25405  dfon2  25411  trpredrec  25508  frmin  25509  wfrlem4  25533  wsuclem  25568  frrlem4  25577  nocvxminlem  25637  nocvxmin  25638  nofulllem5  25653  elfuns  25752  brbtwn2  25836  axeuclidlem  25893  axcontlem9  25903  axcontlem10  25904  btwnswapid  25943  ifscgr  25970  hilbert1.2  26081  supadd  26229  ltflcei  26231  mblfinlem2  26235  elicc3  26311  tailfb  26397  fzmul  26435  metf1o  26452  ismtycnv  26502  ismtyres  26508  crngohomfo  26607  prtlem50  26685  pm11.59  27558  infrglb  27689  afvres  28003  swrdnd  28154  swrdvalodmlem1  28159  swrdccatin2  28176  usgra2wlkspthlem2  28260  usgra2adedgspthlem1  28266  usgra2adedgwlkon  28270  usg2wlkonot  28303  usg2wotspth  28304  2pthfrgrarn2  28337  frgranbnb  28347  lubunNEW  29708  hlhgt2  30123  hl2at  30139  2llnjN  30301  2lplnj  30354  linepsubN  30486  cdlemg33b0  31435  dvh3dim3N  32184  mapdh9a  32525
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 178  df-an 361
  Copyright terms: Public domain W3C validator