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  4785  prel12g  4822  disjiun  5088  soss  5560  wess  5618  frinxp  5715  trin2  6088  xp11  6141  oneqmini  6378  funss  6519  fvcofneq  7047  dff13  7210  f1cofveqaeq  7213  f1eqcocnv  7257  isores3  7291  isosolem  7303  isowe2  7306  trom  7827  f1oweALT  7926  f1o2ndf1  8074  suppofssd  8155  tposfn2  8200  tposf1o2  8204  frrlem4  8241  smo11  8306  tz7.48lem  8382  om00  8512  omsmo  8596  ixpfi2  9262  elfiun  9345  supmo  9367  infmo  9412  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  11308  lemul12b  12010  lbreu  12104  supadd  12122  supmullem2  12125  cju  12153  nnind  12175  uz11  12788  xrre2  13097  qbtwnre  13126  ico0  13319  ioc0  13320  ssfzoulel  13688  ishashinf  14398  swrdccatin2  14664  coss12d  14907  01sqrexlem6  15182  o1lo1  15472  ruclem9  16175  isprm3  16622  eulerthlem2  16721  prmdiveq  16725  ramub2  16954  cictr  17741  clatl  18443  lubun  18450  ipodrsima  18476  dirtr  18537  smndex1mgm  18844  smndex1sgrp  18845  smndex1mnd  18847  mulgpropd  19058  imasabl  19817  dprdss  19972  subrgdvds  20531  rhmsscrnghm  20610  dmatsubcl  22454  scmatcrng  22477  epttop  22965  cnprest  23245  lmmo  23336  lly1stc  23452  txcnp  23576  addcnlem  24821  clmvscom  25058  caussi  25265  bcthlem5  25296  ovollb2lem  25457  voliunlem1  25519  ioombl1lem4  25530  rolle  25962  c1lip1  25970  c1lip3  25972  ulmval  26357  sqf11  27117  fsumvma  27192  dchrelbas3  27217  nocvxminlem  27762  nocvxmin  27763  conway  27787  cofcut1  27928  precsexlem10  28224  acopy  28917  brbtwn2  28990  axeuclidlem  29047  axcontlem9  29057  axcontlem10  29058  umgrvad2edg  29298  upgrwlkdvdelem  29821  usgr2wlkneq  29841  2wlkdlem6  30016  umgr2adedgwlklem  30029  umgr2adedgspth  30033  2pthfrgrrn2  30370  frgrnbnb  30380  fusgr2wsp2nb  30421  nmcvcn  30782  sspmval  30820  sspimsval  30825  shsubcl  31307  shorth  31382  5oalem6  31746  strlem1  32337  atexch  32468  cdj3i  32528  xrofsup  32857  nnindf  32910  cnre2csqima  34088  nummin  35268  subgrwlk  35345  cusgr3cyclex  35349  erdszelem9  35412  erdsze2lem2  35417  gonarlem  35607  satffunlem  35614  satefvfmla1  35638  ss2mcls  35781  funpsstri  35979  dfon2lem4  35997  dfon2  36003  wsuclem  36036  elfuns  36126  btwnswapid  36230  ifscgr  36257  hilbert1.2  36368  elicc3  36530  tailfb  36590  bj-nnfand  36987  bj-gabss  37174  bj-imdirval3  37428  pibt2  37661  wl-mo3t  37820  ltflcei  37848  tan2h  37852  mblfinlem3  37899  fzmul  37981  metf1o  37995  ismtycnv  38042  ismtyres  38048  crngohomfo  38246  cossss  38755  funALTVss  39024  disjss  39071  hlhgt2  39754  hl2at  39770  2llnjN  39932  2lplnj  39985  linepsubN  40117  cdlemg33b0  41066  dvh3dim3N  41814  mapdh9a  42154  fltaccoprm  42987  iocinico  43558  clcnvlem  43968  ismnushort  44646  pm11.59  44736  f1cof1b  47426  afvres  47521  afv2res  47588  isuspgrim0lem  48242  isuspgrimlem  48244  grlimprclnbgrvtx  48348  ply1mulgsumlem1  48735  fldivexpfllog2  48914