Theorem anim12d 609

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 608	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anim12d1  610  anim1d  611  anim2d  612  anim12dan  619  3anim123d  1445  mo3  2564  2euswapv  2630  2euswap  2645  disj  4430  ssunsn2  4808  prel12g  4845  disjiun  5112  soss  5586  wess  5645  frinxp  5742  trin2  6117  xp11  6169  oneqmini  6410  funss  6560  fvcofneq  7088  dff13  7252  f1cofveqaeq  7255  f1eqcocnv  7299  isores3  7333  isosolem  7345  isowe2  7348  trom  7875  f1oweALT  7976  f1o2ndf1  8126  suppofssd  8207  tposfn2  8252  tposf1o2  8256  frrlem4  8293  wfrlem4OLD  8331  smo11  8383  tz7.48lem  8460  om00  8592  omsmo  8675  ixpfi2  9367  elfiun  9447  supmo  9469  infmo  9514  frmin  9768  cardaleph  10108  dfac5  10148  fin1a2lem9  10427  axdc3lem2  10470  zorn2lem6  10520  indpi  10926  genpnmax  11026  reclem3pr  11068  reclem4pr  11069  suplem1pr  11071  supsrlem  11130  dedekind  11403  lemul12b  12103  lbreu  12197  supadd  12215  supmullem2  12218  cju  12241  nnind  12263  uz11  12882  xrre2  13191  qbtwnre  13220  ico0  13413  ioc0  13414  ssfzoulel  13781  ishashinf  14486  swrdccatin2  14752  coss12d  14996  01sqrexlem6  15271  o1lo1  15558  ruclem9  16261  isprm3  16707  eulerthlem2  16806  prmdiveq  16810  ramub2  17039  cictr  17823  clatl  18523  lubun  18530  ipodrsima  18556  dirtr  18617  smndex1mgm  18890  smndex1sgrp  18891  smndex1mnd  18893  mulgpropd  19104  imasabl  19862  dprdss  20017  subrgdvds  20551  rhmsscrnghm  20630  dmatsubcl  22441  scmatcrng  22464  epttop  22952  cnprest  23232  lmmo  23323  lly1stc  23439  txcnp  23563  addcnlem  24809  clmvscom  25046  caussi  25254  bcthlem5  25285  ovollb2lem  25446  voliunlem1  25508  ioombl1lem4  25519  rolle  25951  c1lip1  25959  c1lip3  25961  ulmval  26346  sqf11  27106  fsumvma  27181  dchrelbas3  27206  nocvxminlem  27746  nocvxmin  27747  conway  27768  cofcut1  27885  precsexlem10  28175  acopy  28817  brbtwn2  28889  axeuclidlem  28946  axcontlem9  28956  axcontlem10  28957  umgrvad2edg  29197  upgrwlkdvdelem  29723  usgr2wlkneq  29743  2wlkdlem6  29918  umgr2adedgwlklem  29931  umgr2adedgspth  29935  2pthfrgrrn2  30269  frgrnbnb  30279  fusgr2wsp2nb  30320  nmcvcn  30681  sspmval  30719  sspimsval  30724  shsubcl  31206  shorth  31281  5oalem6  31645  strlem1  32236  atexch  32367  cdj3i  32427  xrofsup  32749  nnindf  32803  cnre2csqima  33947  nummin  35127  subgrwlk  35159  cusgr3cyclex  35163  erdszelem9  35226  erdsze2lem2  35231  gonarlem  35421  satffunlem  35428  satefvfmla1  35452  ss2mcls  35595  funpsstri  35788  dfon2lem4  35809  dfon2  35815  wsuclem  35848  elfuns  35938  btwnswapid  36040  ifscgr  36067  hilbert1.2  36178  elicc3  36340  tailfb  36400  bj-nnfand  36772  bj-gabss  36958  bj-imdirval3  37207  pibt2  37440  wl-mo3t  37599  ltflcei  37637  tan2h  37641  mblfinlem3  37688  fzmul  37770  metf1o  37784  ismtycnv  37831  ismtyres  37837  crngohomfo  38035  cossss  38448  funALTVss  38722  disjss  38754  hlhgt2  39413  hl2at  39429  2llnjN  39591  2lplnj  39644  linepsubN  39776  cdlemg33b0  40725  dvh3dim3N  41473  mapdh9a  41813  fltaccoprm  42638  iocinico  43211  clcnvlem  43622  ismnushort  44300  pm11.59  44390  f1cof1b  47086  afvres  47181  afv2res  47248  isuspgrim0lem  47886  isuspgrimlem  47888  ply1mulgsumlem1  48342  fldivexpfllog2  48525