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  831  anim12dan  833  3anim123d  1296  mo3  2296  2euswap  2355  ssunsn2  4027  disjiun  4277  soss  4654  wess  4702  ordtri3  4750  oneqmini  4765  frinxp  4899  trin2  5216  xp11  5268  funss  5431  fun  5570  fvcofneq  5846  dff13  5966  f1eqcocnv  5994  isores3  6021  isosolem  6033  isowe2  6036  ordom  6480  f1oweALT  6556  f1o2ndf1  6675  tposfn2  6762  tposf1o2  6766  smo11  6817  tz7.48lem  6888  om00  7006  omsmo  7085  ixpfi2  7601  elfiun  7672  supmo  7694  alephord  8237  cardaleph  8251  dfac5  8290  fin1a2lem9  8569  axdc3lem2  8612  zorn2lem6  8662  grudomon  8976  indpi  9068  genpnmax  9168  reclem3pr  9210  reclem4pr  9211  suplem1pr  9213  supsrlem  9270  dedekind  9525  lemul12b  10178  fimaxre  10269  lbreu  10272  supmullem2  10289  cju  10310  nnind  10332  uz11  10875  xrre2  11134  qbtwnre  11161  xrsupexmnf  11259  xrinfmexpnf  11260  ico0  11338  ioc0  11339  ssfzoulel  11613  swrdnd  12318  swrdccatin2  12370  sqrlem6  12729  o1lo1  13007  ruclem9  13512  isprm3  13764  eulerthlem2  13849  prmdiveq  13853  ramub2  14067  joinfval  15163  meetfval  15177  clatl  15278  lubun  15285  ipodrsima  15327  dirtr  15398  mulgpropd  15651  dprdss  16514  subrgdvds  16857  epttop  18588  cnpresti  18867  cnprest  18868  lmmo  18959  1stcrest  19032  lly1stc  19075  txcnp  19168  addcnlem  20415  caussi  20783  bcthlem5  20814  ovollb2lem  20946  voliunlem1  21006  ioombl1lem4  21017  rolle  21437  c1lip1  21444  c1lip3  21446  ulmval  21820  sqf11  22452  fsumvma  22527  dchrelbas3  22552  brbtwn2  23102  axeuclidlem  23159  axcontlem9  23169  axcontlem10  23170  constr3trllem2  23488  4cycl4v4e  23503  4cycl4dv  23504  eupai  23539  subgoablo  23749  nmcvcn  24041  sspmval  24082  sspival  24087  sspimsval  24089  sspph  24206  shsubcl  24574  shorth  24649  5oalem6  25013  strlem1  25605  atexch  25736  cdj3i  25796  xrge0infss  26004  xrofsup  26006  ishashinf  26036  nnindf  26040  cnre2csqima  26293  erdszelem9  27039  erdsze2lem2  27044  funpsstri  27527  dfon2lem4  27550  dfon2  27556  trpredrec  27653  frmin  27654  wfrlem4  27678  wsuclem  27713  frrlem4  27722  nocvxminlem  27782  nocvxmin  27783  nofulllem5  27798  elfuns  27897  btwnswapid  27999  ifscgr  28026  hilbert1.2  28137  wl-mo3t  28350  supadd  28371  ltflcei  28372  tan2h  28377  mblfinlem3  28383  elicc3  28465  tailfb  28551  fzmul  28589  metf1o  28604  ismtycnv  28654  ismtyres  28660  crngohomfo  28759  prtlem50  28945  iocinico  29540  pm11.59  29597  infrglb  29724  afvres  30031  usgra2wlkspthlem2  30250  usgra2adedgspthlem1  30256  usgra2adedgwlkon  30260  usg2wlkonot  30355  usg2wotspth  30356  2pthfrgrarn2  30555  frgranbnb  30565  dmatsubcl  30800  scmatcrng  30811  hlhgt2  32873  hl2at  32889  2llnjN  33051  2lplnj  33104  linepsubN  33236  cdlemg33b0  34185  dvh3dim3N  34934  mapdh9a  35275