Theorem anim12d 610

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anim12d1  611  anim1d  612  anim2d  613  anim12dan  620  3anim123d  1439  sbimdvOLD  2516  sbimdOLD  2518  mo3  2648  mo4  2650  2euswapv  2715  2euswap  2730  ssunsn2  4762  prel12g  4796  disjiun  5055  soss  5495  wess  5544  frinxp  5636  trin2  5985  xp11  6034  oneqmini  6244  funss  6376  fvcofneq  6861  dff13  7015  f1cofveqaeq  7018  f1eqcocnv  7059  isores3  7090  isosolem  7102  isowe2  7105  ordom  7591  f1oweALT  7675  f1o2ndf1  7820  suppofssd  7869  tposfn2  7916  tposf1o2  7920  wfrlem4  7960  smo11  8003  tz7.48lem  8079  om00  8203  omsmo  8283  ixpfi2  8824  elfiun  8896  supmo  8918  infmo  8961  cardaleph  9517  dfac5  9556  fin1a2lem9  9832  axdc3lem2  9875  zorn2lem6  9925  indpi  10331  genpnmax  10431  reclem3pr  10473  reclem4pr  10474  suplem1pr  10476  supsrlem  10535  dedekind  10805  lemul12b  11499  fimaxreOLD  11587  lbreu  11593  supadd  11611  supmullem2  11614  cju  11636  nnind  11658  uz11  12270  xrre2  12566  qbtwnre  12595  ico0  12787  ioc0  12788  ssfzoulel  13134  ishashinf  13824  swrdccatin2  14093  coss12d  14334  sqrlem6  14609  o1lo1  14896  ruclem9  15593  isprm3  16029  eulerthlem2  16121  prmdiveq  16125  ramub2  16352  cictr  17077  clatl  17728  lubun  17735  ipodrsima  17777  dirtr  17848  smndex1mgm  18074  smndex1sgrp  18075  smndex1mnd  18077  mulgpropd  18271  dprdss  19153  subrgdvds  19551  dmatsubcl  21109  scmatcrng  21132  epttop  21619  cnprest  21899  lmmo  21990  lly1stc  22106  txcnp  22230  addcnlem  23474  clmvscom  23696  caussi  23902  bcthlem5  23933  ovollb2lem  24091  voliunlem1  24153  ioombl1lem4  24164  rolle  24589  c1lip1  24596  c1lip3  24598  ulmval  24970  sqf11  25718  fsumvma  25791  dchrelbas3  25816  acopy  26621  brbtwn2  26693  axeuclidlem  26750  axcontlem9  26760  axcontlem10  26761  umgrvad2edg  26997  upgrwlkdvdelem  27519  usgr2wlkneq  27539  2wlkdlem6  27712  umgr2adedgwlklem  27725  umgr2adedgspth  27729  2pthfrgrrn2  28064  frgrnbnb  28074  fusgr2wsp2nb  28115  nmcvcn  28474  sspmval  28512  sspimsval  28517  shsubcl  28999  shorth  29074  5oalem6  29438  strlem1  30029  atexch  30160  cdj3i  30220  xrofsup  30494  nnindf  30537  cnre2csqima  31156  subgrwlk  32381  cusgr3cyclex  32385  erdszelem9  32448  erdsze2lem2  32453  gonarlem  32643  satffunlem  32650  satefvfmla1  32674  ss2mcls  32817  funpsstri  33010  dfon2lem4  33033  dfon2  33039  trpredrec  33079  frmin  33086  wsuclem  33114  frrlem4  33128  nocvxminlem  33249  nocvxmin  33250  conway  33266  elfuns  33378  btwnswapid  33480  ifscgr  33507  hilbert1.2  33618  elicc3  33667  tailfb  33727  bj-nnfand  34080  bj-imdirval3  34476  pibt2  34700  wl-mo3t  34814  ltflcei  34882  tan2h  34886  mblfinlem3  34933  fzmul  35018  metf1o  35032  ismtycnv  35082  ismtyres  35088  crngohomfo  35286  cossss  35672  funALTVss  35934  disjss  35966  hlhgt2  36527  hl2at  36543  2llnjN  36705  2lplnj  36758  linepsubN  36890  cdlemg33b0  37839  dvh3dim3N  38587  mapdh9a  38927  iocinico  39825  clcnvlem  39990  pm11.59  40730  afvres  43378  afv2res  43445  isomuspgrlem1  43999  isomuspgrlem2c  44002  isomuspgrlem2d  44003  rhmsscrnghm  44304  ply1mulgsumlem1  44447  fldivexpfllog2  44632