Theorem anim12d 617

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 616	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  618  anim1d  619  anim2d  620  anim12dan  627  3anim123d  1458  mo3  2585  2euswapv  2651  2euswap  2666  ssunsn2  4779  prel12g  4816  disjiun  5082  soss  5568  wess  5626  frinxp  5723  trin2  6100  xp11  6150  oneqmini  6388  funss  6529  fvcofneq  7063  dff13  7227  f1cofveqaeq  7230  f1eqcocnv  7274  isores3  7308  isosolem  7320  isowe2  7323  trom  7844  f1oweALT  7942  f1o2ndf1  8089  suppofssd  8171  tposfn2  8216  tposf1o2  8220  frrlem4  8258  smo11  8323  tz7.48lem  8400  om00  8532  omsmo  8616  ixpfi2  9283  elfiun  9366  supmo  9388  infmo  9433  frmin  9697  cardaleph  10035  dfac5  10075  fin1a2lem9  10355  axdc3lem2  10398  zorn2lem6  10448  indpi  10855  genpnmax  10955  reclem3pr  10997  reclem4pr  10998  suplem1pr  11000  supsrlem  11059  dedekind  11336  lemul12b  12038  lbreu  12132  supadd  12150  supmullem2  12153  cju  12181  nnind  12218  uz11  12854  xrre2  13163  qbtwnre  13192  ico0  13385  ioc0  13386  ssfzoulel  13756  ishashinf  14466  swrdccatin2  14732  coss12d  14975  01sqrexlem6  15250  o1lo1  15540  ruclem9  16246  isprm3  16693  eulerthlem2  16793  prmdiveq  16797  ramub2  17026  cictr  17814  clatl  18516  lubun  18523  ipodrsima  18549  dirtr  18610  smndex1mgm  18920  smndex1sgrp  18921  smndex1mnd  18923  mulgpropd  19134  imasabl  19892  dprdss  20047  subrgdvds  20608  rhmsscrnghm  20687  dmatsubcl  22531  scmatcrng  22554  epttop  23042  cnprest  23322  lmmo  23413  lly1stc  23529  txcnp  23653  addcnlem  24898  clmvscom  25125  caussi  25332  bcthlem5  25363  ovollb2lem  25523  voliunlem1  25585  ioombl1lem4  25596  rolle  26025  c1lip1  26032  c1lip3  26034  ulmval  26413  sqf11  27173  fsumvma  27247  dchrelbas3  27272  nocvxminlem  27817  nocvxmin  27818  conway  27842  cofcut1  27983  precsexlem10  28279  acopy  28972  brbtwn2  29045  axeuclidlem  29102  axcontlem9  29112  axcontlem10  29113  umgrvad2edg  29353  upgrwlkdvdelem  29875  usgr2wlkneq  29895  2wlkdlem6  30070  umgr2adedgwlklem  30083  umgr2adedgspth  30087  2pthfrgrrn2  30424  frgrnbnb  30434  fusgr2wsp2nb  30475  nmcvcn  30837  sspmval  30875  sspimsval  30880  shsubcl  31362  shorth  31437  5oalem6  31801  strlem1  32392  atexch  32523  cdj3i  32583  xrofsup  32912  nnindf  32965  cnre2csqima  34162  nummin  35344  subgrwlk  35430  cusgr3cyclex  35434  erdszelem9  35497  erdsze2lem2  35502  gonarlem  35692  satffunlem  35699  satefvfmla1  35723  ss2mcls  35866  funpsstri  36064  dfon2lem4  36082  dfon2  36088  wsuclem  36121  elfuns  36211  btwnswapid  36315  ifscgr  36342  hilbert1.2  36453  elicc3  36625  tailfb  36685  dfttc4lem2  36837  bj-nnfand  37178  bj-gabss  37368  bj-imdirval3  37624  pibt2  37859  wl-mo3t  38027  ltflcei  38055  tan2h  38059  mblfinlem3  38106  fzmul  38188  metf1o  38202  ismtycnv  38249  ismtyres  38255  crngohomfo  38453  cossss  38962  funALTVss  39231  disjss  39278  hlhgt2  39961  hl2at  39977  2llnjN  40139  2lplnj  40192  linepsubN  40324  cdlemg33b0  41273  dvh3dim3N  42021  mapdh9a  42361  fltaccoprm  43170  iocinico  43737  clcnvlem  44147  ismnushort  44825  pm11.59  44915  f1cof1b  47619  afvres  47714  afv2res  47781  isuspgrim0lem  48463  isuspgrimlem  48465  grlimprclnbgrvtx  48569  ply1mulgsumlem1  48956  fldivexpfllog2  49135