Theorem anim12d 585

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	⊢ (𝜑 → (𝜓 → 𝜒))
anim12d.2	⊢ (𝜑 → (𝜃 → 𝜏))

Assertion

Ref	Expression
anim12d	⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))

Proof of Theorem anim12d

Step	Hyp	Ref	Expression
1		anim12d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		anim12d.2	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
3		idd 24	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → (𝜒 ∧ 𝜏)))
4	1, 2, 3	syl2and 499	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  anim12d1  586  anim1d  587  anim2d  588  prth  594  im2anan9  898  anim12dan  900  3anim123d  1446  mo3  2536  2euswap  2577  ssunsn2  4391  disjiun  4672  soss  5082  wess  5130  frinxp  5218  trin2  5554  xp11  5604  ordtri3OLD  5798  oneqmini  5814  funss  5945  fun  6104  fvcofneq  6407  dff13  6552  f1cofveqaeq  6555  f1eqcocnv  6596  isores3  6625  isosolem  6637  isowe2  6640  ordom  7116  f1oweALT  7194  f1o2ndf1  7330  tposfn2  7419  tposf1o2  7423  wfrlem4  7463  smo11  7506  tz7.48lem  7581  om00  7700  omsmo  7779  ixpfi2  8305  elfiun  8377  supmo  8399  infmo  8442  alephord  8936  cardaleph  8950  dfac5  8989  fin1a2lem9  9268  axdc3lem2  9311  zorn2lem6  9361  grudomon  9677  indpi  9767  genpnmax  9867  reclem3pr  9909  reclem4pr  9910  suplem1pr  9912  supsrlem  9970  dedekind  10238  lemul12b  10918  fimaxre  11006  lbreu  11011  supadd  11029  supmullem2  11032  cju  11054  nnind  11076  uz11  11748  xrre2  12039  qbtwnre  12068  xrsupexmnf  12173  xrinfmexpnf  12174  ico0  12259  ioc0  12260  ssfzoulel  12602  ishashinf  13285  swrdccatin2  13533  coss12d  13757  sqrlem6  14032  o1lo1  14312  ruclem9  15011  isprm3  15443  eulerthlem2  15534  prmdiveq  15538  ramub2  15765  cictr  16512  joinfval  17048  meetfval  17062  clatl  17163  lubun  17170  ipodrsima  17212  dirtr  17283  mulgpropd  17631  dprdss  18474  subrgdvds  18842  dmatsubcl  20352  scmatcrng  20375  epttop  20861  cnpresti  21140  cnprest  21141  lmmo  21232  1stcrest  21304  lly1stc  21347  txcnp  21471  addcnlem  22714  clmvscom  22936  caussi  23141  bcthlem5  23171  ovollb2lem  23302  voliunlem1  23364  ioombl1lem4  23375  rolle  23798  c1lip1  23805  c1lip3  23807  ulmval  24179  sqf11  24910  fsumvma  24983  dchrelbas3  25008  acopy  25769  brbtwn2  25830  axeuclidlem  25887  axcontlem9  25897  axcontlem10  25898  umgrvad2edg  26150  upgrwlkdvdelem  26688  usgr2wlkneq  26708  2wlkdlem6  26896  umgr2adedgwlklem  26909  umgr2adedgspth  26913  2pthfrgrrn2  27263  frgrnbnb  27273  fusgr2wsp2nb  27314  nmcvcn  27678  sspmval  27716  sspimsval  27721  sspph  27838  shsubcl  28205  shorth  28282  5oalem6  28646  strlem1  29237  atexch  29368  cdj3i  29428  xrofsup  29661  nnindf  29693  cnre2csqima  30085  erdszelem9  31307  erdsze2lem2  31312  ss2mcls  31591  funpsstri  31789  dfon2lem4  31815  dfon2  31821  trpredrec  31862  frmin  31867  wsuclem  31895  frrlem4  31908  nocvxminlem  32018  nocvxmin  32019  conway  32035  elfuns  32147  btwnswapid  32249  ifscgr  32276  hilbert1.2  32387  elicc3  32436  tailfb  32497  wl-mo3t  33488  ltflcei  33527  tan2h  33531  mblfinlem3  33578  fzmul  33667  metf1o  33681  ismtycnv  33731  ismtyres  33737  crngohomfo  33935  cossss  34320  hlhgt2  34993  hl2at  35009  2llnjN  35171  2lplnj  35224  linepsubN  35356  cdlemg33b0  36306  dvh3dim3N  37055  mapdh9a  37396  iocinico  38114  clcnvlem  38247  pm11.59  38908  afvres  41573  rhmsscrnghm  42351  ply1mulgsumlem1  42499  fldivexpfllog2  42684