Theorem anim12d 621

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 25	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → (𝜒 ∧ 𝜏)))
4	1, 2, 3	syl2and 620	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anim12d1  622  anim1d  623  anim2d  624  anim12dan  631  3anim123d  1471  mo3  2589  2euswapv  2655  2euswap  2670  ssunsn2  4787  prel12g  4823  disjiun  5090  soss  5575  wess  5633  frinxp  5730  trin2  6111  xp11  6162  oneqmini  6405  funss  6546  fvcofneq  7081  dff13  7246  f1cofveqaeq  7249  f1eqcocnv  7297  isores3  7331  isosolem  7343  isowe2  7346  trom  7869  f1oweALT  7967  f1o2ndf1  8116  suppofssd  8198  tposfn2  8243  tposf1o2  8247  frrlem4  8285  smo11  8350  tz7.48lemOLD  8429  om00  8561  omsmo  8645  ixpfi2  9317  elfiun  9400  supmo  9422  infmo  9467  frmin  9731  cardaleph  10140  dfac5  10179  fin1a2lem9  10458  axdc3lem2  10501  zorn2lem6  10551  indpi  10964  genpnmax  11064  reclem3pr  11106  reclem4pr  11107  suplem1pr  11109  supsrlem  11168  dedekind  11445  lemul12b  12144  lbreu  12237  supadd  12255  supmullem2  12258  cju  12286  nnind  12323  uz11  12960  xrre2  13270  qbtwnre  13299  ico0  13492  ioc0  13493  ssfzoulel  13864  ishashinf  14576  swrdccatin2  14846  coss12d  15093  01sqrexlem6  15382  o1lo1  15672  ruclem9  16374  isprm3  16821  eulerthlem2  16921  prmdiveq  16925  ramub2  17154  cictr  17942  clatl  18644  lubun  18651  ipodrsima  18677  dirtr  18738  smndex1mgm  19068  smndex1sgrp  19069  smndex1mnd  19071  mulgpropd  19288  imasabl  20052  dprdss  20207  crngrhmfo  20688  subrgdvds  20800  rhmsscrnghm  20879  dmatsubcl  22775  scmatcrng  22798  epttop  23289  cnprest  23569  lmmo  23660  lly1stc  23777  txcnp  23901  addcnlem  25146  clmvscom  25373  caussi  25580  bcthlem5  25611  ovollb2lem  25771  voliunlem1  25833  ioombl1lem4  25844  rolle  26272  c1lip1  26279  c1lip3  26281  ulmval  26671  sqf11  27430  fsumvma  27504  dchrelbas3  27529  nocvxminlem  28074  nocvxmin  28075  conway  28099  cofcut1  28240  precsexlem10  28536  acopy  29275  brbtwn2  29417  axeuclidlem  29474  axcontlem9  29484  axcontlem10  29485  umgrvad2edg  29728  subgrwlk  30203  upgrwlkdvdelem  30256  usgr2wlkneq  30276  2wlkdlem6  30454  umgr2adedgwlklem  30467  umgr2adedgspth  30471  2pthfrgrrn2  30818  frgrnbnb  30828  fusgr2wsp2nb  30869  nmcvcn  31231  sspmval  31269  sspimsval  31274  shsubcl  31756  shorth  31831  5oalem6  32195  strlem1  32786  atexch  32917  cdj3i  32977  xrofsup  33293  nnindf  33345  cnre2csqima  34477  nummin  35653  ackardcard  35760  cusgr3cyclex  35832  erdszelem9  35885  erdsze2lem2  35890  gonarlem  36080  satffunlem  36087  satefvfmla1  36111  ss2mcls  36254  funpsstri  36452  dfon2lem4  36470  dfon2  36476  wsuclem  36509  elfuns  36599  btwnswapid  36704  ifscgr  36731  hilbert1.2  36842  elicc3  37027  tailfb  37087  dfttc4lem2  37239  bj-nnfand  37579  bj-gabss  37770  bj-imdirval3  38025  pibt2  38260  wl-mo3t  38428  ltflcei  38451  tan2h  38455  mblfinlem3  38497  fzmul  38595  metf1o  38609  ismtycnv  38656  ismtyres  38662  crngohomfo  38860  cossss  39367  funALTVss  39636  disjss  39683  hlhgt2  40366  hl2at  40382  2llnjN  40544  2lplnj  40597  linepsubN  40729  cdlemg33b0  41678  dvh3dim3N  42426  mapdh9a  42766  fltaccoprm  43590  iocinico  44157  clcnvlem  44567  ismnushort  45229  pm11.59  45319  f1cof1b  48069  afvres  48164  afv2res  48231  isuspgrim0lem  48913  isuspgrimlem  48915  grlimprclnbgrvtx  49019  ply1mulgsumlem1  49420  fldivexpfllog2  49599