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 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  611  anim1d  612  anim2d  613  anim12dan  620  3anim123d  1446  mo3  2565  2euswapv  2631  2euswap  2646  ssunsn2  4771  prel12g  4808  disjiun  5074  soss  5559  wess  5617  frinxp  5714  trin2  6087  xp11  6140  oneqmini  6377  funss  6518  fvcofneq  7046  dff13  7209  f1cofveqaeq  7212  f1eqcocnv  7256  isores3  7290  isosolem  7302  isowe2  7305  trom  7826  f1oweALT  7925  f1o2ndf1  8072  suppofssd  8153  tposfn2  8198  tposf1o2  8202  frrlem4  8239  smo11  8304  tz7.48lem  8380  om00  8510  omsmo  8594  ixpfi2  9260  elfiun  9343  supmo  9365  infmo  9410  frmin  9673  cardaleph  10011  dfac5  10051  fin1a2lem9  10330  axdc3lem2  10373  zorn2lem6  10423  indpi  10830  genpnmax  10930  reclem3pr  10972  reclem4pr  10973  suplem1pr  10975  supsrlem  11034  dedekind  11309  lemul12b  12012  lbreu  12106  supadd  12124  supmullem2  12127  cju  12155  nnind  12192  uz11  12813  xrre2  13122  qbtwnre  13151  ico0  13344  ioc0  13345  ssfzoulel  13715  ishashinf  14425  swrdccatin2  14691  coss12d  14934  01sqrexlem6  15209  o1lo1  15499  ruclem9  16205  isprm3  16652  eulerthlem2  16752  prmdiveq  16756  ramub2  16985  cictr  17772  clatl  18474  lubun  18481  ipodrsima  18507  dirtr  18568  smndex1mgm  18878  smndex1sgrp  18879  smndex1mnd  18881  mulgpropd  19092  imasabl  19851  dprdss  20006  subrgdvds  20563  rhmsscrnghm  20642  dmatsubcl  22463  scmatcrng  22486  epttop  22974  cnprest  23254  lmmo  23345  lly1stc  23461  txcnp  23585  addcnlem  24830  clmvscom  25057  caussi  25264  bcthlem5  25295  ovollb2lem  25455  voliunlem1  25517  ioombl1lem4  25528  rolle  25957  c1lip1  25964  c1lip3  25966  ulmval  26345  sqf11  27102  fsumvma  27176  dchrelbas3  27201  nocvxminlem  27746  nocvxmin  27747  conway  27771  cofcut1  27912  precsexlem10  28208  acopy  28901  brbtwn2  28974  axeuclidlem  29031  axcontlem9  29041  axcontlem10  29042  umgrvad2edg  29282  upgrwlkdvdelem  29804  usgr2wlkneq  29824  2wlkdlem6  29999  umgr2adedgwlklem  30012  umgr2adedgspth  30016  2pthfrgrrn2  30353  frgrnbnb  30363  fusgr2wsp2nb  30404  nmcvcn  30766  sspmval  30804  sspimsval  30809  shsubcl  31291  shorth  31366  5oalem6  31730  strlem1  32321  atexch  32452  cdj3i  32512  xrofsup  32840  nnindf  32893  cnre2csqima  34055  nummin  35236  subgrwlk  35314  cusgr3cyclex  35318  erdszelem9  35381  erdsze2lem2  35386  gonarlem  35576  satffunlem  35583  satefvfmla1  35607  ss2mcls  35750  funpsstri  35948  dfon2lem4  35966  dfon2  35972  wsuclem  36005  elfuns  36095  btwnswapid  36199  ifscgr  36226  hilbert1.2  36337  elicc3  36499  tailfb  36559  dfttc4lem2  36711  bj-nnfand  37052  bj-gabss  37242  bj-imdirval3  37498  pibt2  37733  wl-mo3t  37901  ltflcei  37929  tan2h  37933  mblfinlem3  37980  fzmul  38062  metf1o  38076  ismtycnv  38123  ismtyres  38129  crngohomfo  38327  cossss  38836  funALTVss  39105  disjss  39152  hlhgt2  39835  hl2at  39851  2llnjN  40013  2lplnj  40066  linepsubN  40198  cdlemg33b0  41147  dvh3dim3N  41895  mapdh9a  42235  fltaccoprm  43073  iocinico  43640  clcnvlem  44050  ismnushort  44728  pm11.59  44818  f1cof1b  47519  afvres  47614  afv2res  47681  isuspgrim0lem  48363  isuspgrimlem  48365  grlimprclnbgrvtx  48469  ply1mulgsumlem1  48856  fldivexpfllog2  49035