Theorem anim12d 558

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

Step	Hyp	Ref	Expression
1		anim12d.1	. 2 |- ( ph -> ( ps -> ch ) )
2		anim12d.2	. 2 |- ( ph -> ( th -> ta ) )
3		idd 24	. 2 |- ( ph -> ( ( ch /\ ta ) -> ( ch /\ ta ) ) )
4	1, 2, 3	syl2and 480	1 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  anim1d  559  anim2d  560  prth  566  im2anan9  824  anim12dan  826  3anim123d  1289  mo3  2292  2euswap  2353  ssunsn2  4020  disjiun  4270  soss  4646  wess  4694  ordtri3  4742  oneqmini  4757  frinxp  4891  trin2  5209  xp11  5261  funss  5424  fun  5563  fvcofneq  5839  dff13  5958  f1eqcocnv  5986  isores3  6013  isosolem  6025  isowe2  6028  ordom  6474  f1oweALT  6550  f1o2ndf1  6669  tposfn2  6756  tposf1o2  6760  smo11  6811  tz7.48lem  6882  om00  7002  omsmo  7081  ixpfi2  7597  elfiun  7668  supmo  7690  alephord  8233  cardaleph  8247  dfac5  8286  fin1a2lem9  8565  axdc3lem2  8608  zorn2lem6  8658  grudomon  8971  indpi  9063  genpnmax  9163  reclem3pr  9205  reclem4pr  9206  suplem1pr  9208  supsrlem  9265  dedekind  9520  lemul12b  10173  fimaxre  10264  lbreu  10267  supmullem2  10284  cju  10305  nnind  10327  uz11  10870  xrre2  11129  qbtwnre  11156  xrsupexmnf  11254  xrinfmexpnf  11255  ico0  11333  ioc0  11334  ssfzoulel  11604  swrdnd  12309  swrdccatin2  12361  sqrlem6  12720  o1lo1  12998  ruclem9  13502  isprm3  13754  eulerthlem2  13839  prmdiveq  13843  ramub2  14057  joinfval  15153  meetfval  15167  clatl  15268  lubun  15275  ipodrsima  15317  dirtr  15388  mulgpropd  15639  dprdss  16499  subrgdvds  16802  epttop  18454  cnpresti  18733  cnprest  18734  lmmo  18825  1stcrest  18898  lly1stc  18941  txcnp  19034  addcnlem  20281  caussi  20649  bcthlem5  20680  ovollb2lem  20812  voliunlem1  20872  ioombl1lem4  20883  rolle  21303  c1lip1  21310  c1lip3  21312  ulmval  21729  sqf11  22361  fsumvma  22436  dchrelbas3  22461  brbtwn2  22973  axeuclidlem  23030  axcontlem9  23040  axcontlem10  23041  constr3trllem2  23359  4cycl4v4e  23374  4cycl4dv  23375  eupai  23410  subgoablo  23620  nmcvcn  23912  sspmval  23953  sspival  23958  sspimsval  23960  sspph  24077  shsubcl  24445  shorth  24520  5oalem6  24884  strlem1  25476  atexch  25607  cdj3i  25667  xrofsup  25877  ishashinf  25907  nnindf  25911  cnre2csqima  26194  erdszelem9  26934  erdsze2lem2  26939  funpsstri  27422  dfon2lem4  27445  dfon2  27451  trpredrec  27548  frmin  27549  wfrlem4  27573  wsuclem  27608  frrlem4  27617  nocvxminlem  27677  nocvxmin  27678  nofulllem5  27693  elfuns  27792  btwnswapid  27894  ifscgr  27921  hilbert1.2  28032  supadd  28259  ltflcei  28260  tan2h  28265  mblfinlem3  28271  elicc3  28353  tailfb  28439  fzmul  28477  metf1o  28492  ismtycnv  28542  ismtyres  28548  crngohomfo  28647  prtlem50  28834  iocinico  29429  pm11.59  29486  infrglb  29614  afvres  29921  usgra2wlkspthlem2  30140  usgra2adedgspthlem1  30146  usgra2adedgwlkon  30150  usg2wlkonot  30245  usg2wotspth  30246  2pthfrgrarn2  30445  frgranbnb  30455  hlhgt2  32603  hl2at  32619  2llnjN  32781  2lplnj  32834  linepsubN  32966  cdlemg33b0  33915  dvh3dim3N  34664  mapdh9a  35005