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  1297  mo3  2307  2euswap  2366  2moOLD  2370  ssunsn2  4143  disjiun  4393  soss  4770  wess  4818  ordtri3  4866  oneqmini  4881  frinxp  5015  trin2  5332  xp11  5384  funss  5547  fun  5686  fvcofneq  5963  dff13  6083  f1eqcocnv  6111  isores3  6138  isosolem  6150  isowe2  6153  ordom  6598  f1oweALT  6674  f1o2ndf1  6793  tposfn2  6880  tposf1o2  6884  smo11  6938  tz7.48lem  7009  om00  7127  omsmo  7206  ixpfi2  7723  elfiun  7794  supmo  7816  alephord  8359  cardaleph  8373  dfac5  8412  fin1a2lem9  8691  axdc3lem2  8734  zorn2lem6  8784  grudomon  9098  indpi  9190  genpnmax  9290  reclem3pr  9332  reclem4pr  9333  suplem1pr  9335  supsrlem  9392  dedekind  9647  lemul12b  10300  fimaxre  10391  lbreu  10394  supmullem2  10411  cju  10432  nnind  10454  uz11  10997  xrre2  11256  qbtwnre  11283  xrsupexmnf  11381  xrinfmexpnf  11382  ico0  11460  ioc0  11461  ssfzoulel  11741  swrdnd  12447  swrdccatin2  12499  sqrlem6  12858  o1lo1  13136  ruclem9  13641  isprm3  13893  eulerthlem2  13978  prmdiveq  13982  ramub2  14196  joinfval  15293  meetfval  15307  clatl  15408  lubun  15415  ipodrsima  15457  dirtr  15528  mulgpropd  15782  dprdss  16651  subrgdvds  17005  epttop  18748  cnpresti  19027  cnprest  19028  lmmo  19119  1stcrest  19192  lly1stc  19235  txcnp  19328  addcnlem  20575  caussi  20943  bcthlem5  20974  ovollb2lem  21106  voliunlem1  21167  ioombl1lem4  21178  rolle  21598  c1lip1  21605  c1lip3  21607  ulmval  21981  sqf11  22613  fsumvma  22688  dchrelbas3  22713  brbtwn2  23323  axeuclidlem  23380  axcontlem9  23390  axcontlem10  23391  constr3trllem2  23709  4cycl4v4e  23724  4cycl4dv  23725  eupai  23760  subgoablo  23970  nmcvcn  24262  sspmval  24303  sspival  24308  sspimsval  24310  sspph  24427  shsubcl  24795  shorth  24870  5oalem6  25234  strlem1  25826  atexch  25957  cdj3i  26017  xrge0infss  26224  xrofsup  26226  ishashinf  26250  nnindf  26254  cnre2csqima  26506  erdszelem9  27251  erdsze2lem2  27256  funpsstri  27740  dfon2lem4  27763  dfon2  27769  trpredrec  27866  frmin  27867  wfrlem4  27891  wsuclem  27926  frrlem4  27935  nocvxminlem  27995  nocvxmin  27996  nofulllem5  28011  elfuns  28110  btwnswapid  28212  ifscgr  28239  hilbert1.2  28350  wl-mo3t  28565  supadd  28586  ltflcei  28587  tan2h  28592  mblfinlem3  28598  elicc3  28680  tailfb  28766  fzmul  28804  metf1o  28819  ismtycnv  28869  ismtyres  28875  crngohomfo  28974  prtlem50  29160  iocinico  29755  pm11.59  29812  infrglb  29939  afvres  30246  usgra2wlkspthlem2  30465  usgra2adedgspthlem1  30471  usgra2adedgwlkon  30475  usg2wlkonot  30570  usg2wotspth  30571  2pthfrgrarn2  30770  frgranbnb  30780  ply1mulgsumlem1  31018  dmatsubcl  31076  scmatcrng  31087  hlhgt2  33391  hl2at  33407  2llnjN  33569  2lplnj  33622  linepsubN  33754  cdlemg33b0  34703  dvh3dim3N  35452  mapdh9a  35793