Theorem anim12d 566

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 25	. 2 |- ( ph -> ( ( ch /\ ta ) -> ( ch /\ ta ) ) )
4	1, 2, 3	syl2and 486	1 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )

Syntax hints:   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  anim12d1  567  anim1d  568  anim2d  569  prth  575  im2anan9  846  anim12dan  848  3anim123d  1346  mo3  2336  2euswap  2377  ssunsn2  4131  disjiun  4393  soss  4773  wess  4821  frinxp  4900  trin2  5223  xp11  5272  ordtri3  5459  oneqmini  5474  funss  5600  fun  5746  fvcofneq  6030  dff13  6159  f1eqcocnv  6199  isores3  6226  isosolem  6238  isowe2  6241  ordom  6701  f1oweALT  6777  f1o2ndf1  6904  tposfn2  6995  tposf1o2  6999  wfrlem4  7039  smo11  7083  tz7.48lem  7158  om00  7276  omsmo  7355  ixpfi2  7872  elfiun  7944  supmo  7966  infmo  8011  alephord  8506  cardaleph  8520  dfac5  8559  fin1a2lem9  8838  axdc3lem2  8881  zorn2lem6  8931  grudomon  9242  indpi  9332  genpnmax  9432  reclem3pr  9474  reclem4pr  9475  suplem1pr  9477  supsrlem  9535  dedekind  9797  lemul12b  10462  fimaxre  10551  lbreu  10556  supadd  10575  supmullem2  10578  cju  10605  nnind  10627  uz11  11181  xrre2  11465  qbtwnre  11492  xrsupexmnf  11590  xrinfmexpnf  11591  ico0  11682  ioc0  11683  ssfzoulel  12005  ishashinf  12626  swrdccatin2  12843  coss12d  13036  sqrlem6  13311  o1lo1  13601  ruclem9  14290  isprm3  14633  eulerthlem2  14730  prmdiveq  14734  ramub2  14971  cictr  15710  joinfval  16247  meetfval  16261  clatl  16362  lubun  16369  ipodrsima  16411  dirtr  16482  mulgpropd  16791  dprdss  17662  subrgdvds  18022  dmatsubcl  19523  scmatcrng  19546  epttop  20024  cnpresti  20304  cnprest  20305  lmmo  20396  1stcrest  20468  lly1stc  20511  txcnp  20635  addcnlem  21896  caussi  22267  bcthlem5  22296  ovollb2lem  22441  voliunlem1  22503  ioombl1lem4  22514  rolle  22942  c1lip1  22949  c1lip3  22951  ulmval  23335  sqf11  24066  fsumvma  24141  dchrelbas3  24166  acopy  24874  brbtwn2  24935  axeuclidlem  24992  axcontlem9  25002  axcontlem10  25003  usgra2adedgspthlem1  25339  usgra2adedgwlkon  25343  usgra2wlkspthlem2  25348  constr3trllem2  25379  4cycl4v4e  25394  4cycl4dv  25395  usg2wlkonot  25611  usg2wotspth  25612  eupai  25695  2pthfrgrarn2  25738  frgranbnb  25748  subgoablo  26039  nmcvcn  26331  sspmval  26372  sspival  26377  sspimsval  26379  sspph  26496  shsubcl  26873  shorth  26948  5oalem6  27312  strlem1  27903  atexch  28034  cdj3i  28094  xrge0infssOLD  28341  xrofsup  28353  nnindf  28382  cnre2csqima  28717  erdszelem9  29922  erdsze2lem2  29927  ss2mcls  30206  funpsstri  30406  dfon2lem4  30432  dfon2  30438  trpredrec  30479  frmin  30480  wsuclem  30508  frrlem4  30517  nocvxminlem  30579  nocvxmin  30580  nofulllem5  30595  elfuns  30682  btwnswapid  30784  ifscgr  30811  hilbert1.2  30922  elicc3  30973  tailfb  31033  wl-mo3t  31905  ltflcei  31933  tan2h  31937  mblfinlem3  31979  fzmul  32069  metf1o  32084  ismtycnv  32134  ismtyres  32140  crngohomfo  32239  hlhgt2  32954  hl2at  32970  2llnjN  33132  2lplnj  33185  linepsubN  33317  cdlemg33b0  34268  dvh3dim3N  35017  mapdh9a  35358  iocinico  36096  clcnvlem  36230  pm11.59  36741  infrglbOLD  37669  afvres  38674  upgrspths1wlklem  39696  usgvad2edg  39776  rhmsscrnghm  40081  ply1mulgsumlem1  40231  fldivexpfllog2  40429