Theorem anim12d 599

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 598	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  anim12d1  600  anim1d  601  anim2d  602  anim12dan  609  im2anan9  610  prth  796  3anim123d  1422  sbimdvOLD  2436  sbimdOLD  2439  mo3  2577  mo3OLD  2578  2euswapv  2663  2euswap  2676  ssunsn2  4634  prel12g  4668  disjiun  4917  soss  5345  wess  5394  frinxp  5484  trin2  5823  xp11  5872  oneqmini  6080  funss  6207  fvcofneq  6684  dff13  6838  f1cofveqaeq  6841  f1eqcocnv  6882  isores3  6911  isosolem  6923  isowe2  6926  ordom  7405  f1oweALT  7485  f1o2ndf1  7623  suppofssd  7670  tposfn2  7717  tposf1o2  7721  wfrlem4  7761  wfrlem4OLD  7762  smo11  7805  tz7.48lem  7880  om00  8002  omsmo  8081  ixpfi2  8617  elfiun  8689  supmo  8711  infmo  8754  cardaleph  9309  dfac5  9348  fin1a2lem9  9628  axdc3lem2  9671  zorn2lem6  9721  indpi  10127  genpnmax  10227  reclem3pr  10269  reclem4pr  10270  suplem1pr  10272  supsrlem  10331  dedekind  10603  lemul12b  11298  fimaxreOLD  11386  lbreu  11392  supadd  11410  supmullem2  11413  cju  11435  nnind  11459  uz11  12081  xrre2  12380  qbtwnre  12409  ico0  12600  ioc0  12601  ssfzoulel  12946  ishashinf  13634  swrdccatin2  13929  coss12d  14193  sqrlem6  14468  o1lo1  14755  ruclem9  15451  isprm3  15883  eulerthlem2  15975  prmdiveq  15979  ramub2  16206  cictr  16933  clatl  17584  lubun  17591  ipodrsima  17633  dirtr  17704  mulgpropd  18053  dprdss  18901  subrgdvds  19272  dmatsubcl  20811  scmatcrng  20834  epttop  21321  cnprest  21601  lmmo  21692  lly1stc  21808  txcnp  21932  addcnlem  23175  clmvscom  23397  caussi  23603  bcthlem5  23634  ovollb2lem  23792  voliunlem1  23854  ioombl1lem4  23865  rolle  24290  c1lip1  24297  c1lip3  24299  ulmval  24671  sqf11  25418  fsumvma  25491  dchrelbas3  25516  acopy  26322  brbtwn2  26394  axeuclidlem  26451  axcontlem9  26461  axcontlem10  26462  umgrvad2edg  26698  upgrwlkdvdelem  27225  usgr2wlkneq  27245  2wlkdlem6  27437  umgr2adedgwlklem  27450  umgr2adedgspth  27454  2pthfrgrrn2  27817  frgrnbnb  27827  fusgr2wsp2nb  27868  nmcvcn  28249  sspmval  28287  sspimsval  28292  sspphOLD  28409  shsubcl  28776  shorth  28853  5oalem6  29217  strlem1  29808  atexch  29939  cdj3i  29999  xrofsup  30251  nnindf  30288  cnre2csqima  30804  erdszelem9  32037  erdsze2lem2  32042  ss2mcls  32341  funpsstri  32534  dfon2lem4  32557  dfon2  32563  trpredrec  32604  frmin  32611  wsuclem  32639  frrlem4  32653  nocvxminlem  32774  nocvxmin  32775  conway  32791  elfuns  32903  btwnswapid  33005  ifscgr  33032  hilbert1.2  33143  elicc3  33192  tailfb  33252  pibt2  34145  wl-mo3t  34259  ltflcei  34327  tan2h  34331  mblfinlem3  34378  fzmul  34464  metf1o  34478  ismtycnv  34528  ismtyres  34534  crngohomfo  34732  cossss  35121  funALTVss  35383  disjss  35415  hlhgt2  35976  hl2at  35992  2llnjN  36154  2lplnj  36207  linepsubN  36339  cdlemg33b0  37288  dvh3dim3N  38036  mapdh9a  38376  iocinico  39220  clcnvlem  39352  pm11.59  40146  afvres  42783  afv2res  42850  isomuspgrlem1  43366  isomuspgrlem2c  43369  isomuspgrlem2d  43370  rhmsscrnghm  43667  ply1mulgsumlem1  43813  fldivexpfllog2  43999