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  2512  sbimdOLD  2514  mo3  2644  mo4  2646  2euswapv  2711  2euswap  2726  ssunsn2  4753  prel12g  4787  disjiun  5045  soss  5487  wess  5536  frinxp  5628  trin2  5977  xp11  6026  oneqmini  6236  funss  6368  fvcofneq  6853  dff13  7007  f1cofveqaeq  7010  f1eqcocnv  7051  isores3  7082  isosolem  7094  isowe2  7097  ordom  7583  f1oweALT  7667  f1o2ndf1  7812  suppofssd  7861  tposfn2  7908  tposf1o2  7912  wfrlem4  7952  smo11  7995  tz7.48lem  8071  om00  8195  omsmo  8275  ixpfi2  8816  elfiun  8888  supmo  8910  infmo  8953  cardaleph  9509  dfac5  9548  fin1a2lem9  9824  axdc3lem2  9867  zorn2lem6  9917  indpi  10323  genpnmax  10423  reclem3pr  10465  reclem4pr  10466  suplem1pr  10468  supsrlem  10527  dedekind  10797  lemul12b  11491  fimaxreOLD  11579  lbreu  11585  supadd  11603  supmullem2  11606  cju  11628  nnind  11650  uz11  12261  xrre2  12557  qbtwnre  12586  ico0  12778  ioc0  12779  ssfzoulel  13125  ishashinf  13815  swrdccatin2  14085  coss12d  14326  sqrlem6  14601  o1lo1  14888  ruclem9  15585  isprm3  16021  eulerthlem2  16113  prmdiveq  16117  ramub2  16344  cictr  17069  clatl  17720  lubun  17727  ipodrsima  17769  dirtr  17840  smndex1mgm  18066  smndex1sgrp  18067  smndex1mnd  18069  mulgpropd  18263  dprdss  19145  subrgdvds  19543  dmatsubcl  21101  scmatcrng  21124  epttop  21611  cnprest  21891  lmmo  21982  lly1stc  22098  txcnp  22222  addcnlem  23466  clmvscom  23688  caussi  23894  bcthlem5  23925  ovollb2lem  24083  voliunlem1  24145  ioombl1lem4  24156  rolle  24581  c1lip1  24588  c1lip3  24590  ulmval  24962  sqf11  25710  fsumvma  25783  dchrelbas3  25808  acopy  26613  brbtwn2  26685  axeuclidlem  26742  axcontlem9  26752  axcontlem10  26753  umgrvad2edg  26989  upgrwlkdvdelem  27511  usgr2wlkneq  27531  2wlkdlem6  27704  umgr2adedgwlklem  27717  umgr2adedgspth  27721  2pthfrgrrn2  28056  frgrnbnb  28066  fusgr2wsp2nb  28107  nmcvcn  28466  sspmval  28504  sspimsval  28509  shsubcl  28991  shorth  29066  5oalem6  29430  strlem1  30021  atexch  30152  cdj3i  30212  xrofsup  30486  nnindf  30529  cnre2csqima  31149  subgrwlk  32374  cusgr3cyclex  32378  erdszelem9  32441  erdsze2lem2  32446  gonarlem  32636  satffunlem  32643  satefvfmla1  32667  ss2mcls  32810  funpsstri  33003  dfon2lem4  33026  dfon2  33032  trpredrec  33072  frmin  33079  wsuclem  33107  frrlem4  33121  nocvxminlem  33242  nocvxmin  33243  conway  33259  elfuns  33371  btwnswapid  33473  ifscgr  33500  hilbert1.2  33611  elicc3  33660  tailfb  33720  bj-nnfand  34073  bj-imdirval3  34468  pibt2  34692  wl-mo3t  34806  ltflcei  34874  tan2h  34878  mblfinlem3  34925  fzmul  35010  metf1o  35024  ismtycnv  35074  ismtyres  35080  crngohomfo  35278  cossss  35664  funALTVss  35926  disjss  35958  hlhgt2  36519  hl2at  36535  2llnjN  36697  2lplnj  36750  linepsubN  36882  cdlemg33b0  37831  dvh3dim3N  38579  mapdh9a  38919  iocinico  39811  clcnvlem  39976  pm11.59  40716  afvres  43365  afv2res  43432  isomuspgrlem1  43986  isomuspgrlem2c  43989  isomuspgrlem2d  43990  rhmsscrnghm  44291  ply1mulgsumlem1  44434  fldivexpfllog2  44619