Theorem anim12d 563

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 483	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  564  anim2d  565  prth  571  im2anan9  835  anim12dan  837  3anim123d  1307  mo3  2309  2euswap  2356  2moOLD  2360  ssunsn2  4174  disjiun  4427  soss  4808  wess  4856  ordtri3  4904  oneqmini  4919  frinxp  5055  trin2  5380  xp11  5432  funss  5596  fun  5738  fvcofneq  6024  dff13  6151  f1eqcocnv  6189  isores3  6216  isosolem  6228  isowe2  6231  ordom  6694  f1oweALT  6769  f1o2ndf1  6893  tposfn2  6979  tposf1o2  6983  smo11  7037  tz7.48lem  7108  om00  7226  omsmo  7305  ixpfi2  7820  elfiun  7892  supmo  7914  alephord  8459  cardaleph  8473  dfac5  8512  fin1a2lem9  8791  axdc3lem2  8834  zorn2lem6  8884  grudomon  9198  indpi  9288  genpnmax  9388  reclem3pr  9430  reclem4pr  9431  suplem1pr  9433  supsrlem  9491  dedekind  9747  lemul12b  10406  fimaxre  10497  lbreu  10500  supmullem2  10517  cju  10539  nnind  10561  uz11  11114  xrre2  11382  qbtwnre  11409  xrsupexmnf  11507  xrinfmexpnf  11508  ico0  11586  ioc0  11587  ssfzoulel  11888  swrdnd  12639  swrdccatin2  12694  sqrlem6  13063  o1lo1  13342  ruclem9  13953  isprm3  14208  eulerthlem2  14294  prmdiveq  14298  ramub2  14514  joinfval  15610  meetfval  15624  clatl  15725  lubun  15732  ipodrsima  15774  dirtr  15845  mulgpropd  16154  dprdss  17055  subrgdvds  17422  dmatsubcl  18978  scmatcrng  19001  epttop  19488  cnpresti  19767  cnprest  19768  lmmo  19859  1stcrest  19932  lly1stc  19975  txcnp  20099  addcnlem  21346  caussi  21714  bcthlem5  21745  ovollb2lem  21877  voliunlem1  21938  ioombl1lem4  21949  rolle  22369  c1lip1  22376  c1lip3  22378  ulmval  22753  sqf11  23391  fsumvma  23466  dchrelbas3  23491  brbtwn2  24186  axeuclidlem  24243  axcontlem9  24253  axcontlem10  24254  usgra2adedgspthlem1  24589  usgra2adedgwlkon  24593  usgra2wlkspthlem2  24598  constr3trllem2  24629  4cycl4v4e  24644  4cycl4dv  24645  usg2wlkonot  24861  usg2wotspth  24862  eupai  24945  2pthfrgrarn2  24988  frgranbnb  24998  subgoablo  25291  nmcvcn  25583  sspmval  25624  sspival  25629  sspimsval  25631  sspph  25748  shsubcl  26116  shorth  26191  5oalem6  26555  strlem1  27147  atexch  27278  cdj3i  27338  xrge0infss  27558  xrofsup  27560  ishashinf  27584  nnindf  27588  cnre2csqima  27871  erdszelem9  28621  erdsze2lem2  28626  ss2mcls  28906  funpsstri  29171  dfon2lem4  29194  dfon2  29200  trpredrec  29297  frmin  29298  wfrlem4  29322  wsuclem  29357  frrlem4  29366  nocvxminlem  29426  nocvxmin  29427  nofulllem5  29442  elfuns  29541  btwnswapid  29643  ifscgr  29670  hilbert1.2  29781  wl-mo3t  29997  supadd  30018  ltflcei  30019  tan2h  30023  mblfinlem3  30029  elicc3  30111  tailfb  30171  fzmul  30209  metf1o  30224  ismtycnv  30274  ismtyres  30280  crngohomfo  30379  prtlem50  30564  iocinico  31155  pm11.59  31251  infrglb  31538  afvres  32211  usgvad2edg  32365  rhmsscrnghm  32706  ply1mulgsumlem1  32856  hlhgt2  34988  hl2at  35004  2llnjN  35166  2lplnj  35219  linepsubN  35351  cdlemg33b0  36302  dvh3dim3N  37051  mapdh9a  37392  coss12d  37597  bj-frege52a  37706