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  2357  ssunsn2  3958  disjiun  4202  soss  4521  wess  4569  ordtri3  4617  oneqmini  4632  ordom  4854  frinxp  4943  trin2  5257  xp11  5304  funss  5472  fun  5607  dff13  6004  f1eqcocnv  6028  isores3  6055  isosolem  6067  isowe2  6070  f1oweALT  6074  f1o2ndf1  6454  tposfn2  6501  tposf1o2  6505  smo11  6626  tfrlem1  6636  tz7.48lem  6698  om00  6818  omsmo  6897  ixpfi2  7405  elfiun  7435  supmo  7457  alephord  7956  cardaleph  7970  dfac5  8009  fin1a2lem9  8288  axdc3lem2  8331  zorn2lem6  8381  grudomon  8692  indpi  8784  genpnmax  8884  reclem3pr  8926  reclem4pr  8927  suplem1pr  8929  supsrlem  8986  lemul12b  9867  fimaxre  9955  lbreu  9958  supmullem2  9975  cju  9996  nnind  10018  uz11  10508  xrre2  10758  qbtwnre  10785  xrsupexmnf  10883  xrinfmexpnf  10884  ico0  10962  ioc0  10963  sqrlem6  12053  o1lo1  12331  ruclem9  12837  isprm3  13088  eulerthlem2  13171  prmdiveq  13175  ramub2  13382  lubun  14550  ipodrsima  14591  spwpr4  14663  dirtr  14681  mulgpropd  14923  dprdss  15587  subrgdvds  15882  epttop  17073  cnpresti  17352  cnprest  17353  lmmo  17444  1stcrest  17516  lly1stc  17559  txcnp  17652  addcnlem  18894  caussi  19250  bcthlem5  19281  ovollb2lem  19384  voliunlem1  19444  ioombl1lem4  19455  rolle  19874  c1lip1  19881  c1lip3  19883  ulmval  20296  sqf11  20922  fsumvma  20997  dchrelbas3  21022  constr3trllem2  21638  4cycl4v4e  21653  4cycl4dv  21654  eupai  21689  subgoablo  21899  nmcvcn  22191  sspmval  22232  sspival  22237  sspimsval  22239  sspph  22356  shsubcl  22723  shorth  22797  5oalem6  23161  strlem1  23753  atexch  23884  cdj3i  23944  xrofsup  24126  ishashinf  24159  cnre2csqima  24309  erdszelem9  24885  erdsze2lem2  24890  dedekind  25187  funpsstri  25389  dfon2lem4  25413  dfon2  25419  trpredrec  25516  frmin  25517  wfrlem4  25541  wsuclem  25576  frrlem4  25585  nocvxminlem  25645  nocvxmin  25646  nofulllem5  25661  elfuns  25760  brbtwn2  25844  axeuclidlem  25901  axcontlem9  25911  axcontlem10  25912  btwnswapid  25951  ifscgr  25978  hilbert1.2  26089  supadd  26238  ltflcei  26239  mblfinlem3  26245  elicc3  26320  tailfb  26406  fzmul  26444  metf1o  26461  ismtycnv  26511  ismtyres  26517  crngohomfo  26616  prtlem50  26694  pm11.59  27567  infrglb  27698  afvres  28012  swrdnd  28182  swrdvalodmlem1  28187  swrdccatin2  28210  usgra2wlkspthlem2  28307  usgra2adedgspthlem1  28313  usgra2adedgwlkon  28317  usg2wlkonot  28350  usg2wotspth  28351  2pthfrgrarn2  28400  frgranbnb  28410  lubunNEW  29771  hlhgt2  30186  hl2at  30202  2llnjN  30364  2lplnj  30417  linepsubN  30549  cdlemg33b0  31498  dvh3dim3N  32247  mapdh9a  32588
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