Theorem anim12d 609

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 608	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  610  anim1d  611  anim2d  612  anim12dan  619  3anim123d  1442  mo3  2562  mo4  2564  2euswapv  2628  2euswap  2643  disj  4456  ssunsn2  4832  prel12g  4869  disjiun  5136  soss  5617  wess  5675  frinxp  5771  trin2  6146  xp11  6197  oneqmini  6438  funss  6587  fvcofneq  7113  dff13  7275  f1cofveqaeq  7278  f1eqcocnv  7321  isores3  7355  isosolem  7367  isowe2  7370  trom  7896  f1oweALT  7996  f1o2ndf1  8146  suppofssd  8227  tposfn2  8272  tposf1o2  8276  frrlem4  8313  wfrlem4OLD  8351  smo11  8403  tz7.48lem  8480  om00  8612  omsmo  8695  ixpfi2  9388  elfiun  9468  supmo  9490  infmo  9533  frmin  9787  cardaleph  10127  dfac5  10167  fin1a2lem9  10446  axdc3lem2  10489  zorn2lem6  10539  indpi  10945  genpnmax  11045  reclem3pr  11087  reclem4pr  11088  suplem1pr  11090  supsrlem  11149  dedekind  11422  lemul12b  12122  lbreu  12216  supadd  12234  supmullem2  12237  cju  12260  nnind  12282  uz11  12901  xrre2  13209  qbtwnre  13238  ico0  13430  ioc0  13431  ssfzoulel  13796  ishashinf  14499  swrdccatin2  14764  coss12d  15008  01sqrexlem6  15283  o1lo1  15570  ruclem9  16271  isprm3  16717  eulerthlem2  16816  prmdiveq  16820  ramub2  17048  cictr  17853  clatl  18566  lubun  18573  ipodrsima  18599  dirtr  18660  smndex1mgm  18933  smndex1sgrp  18934  smndex1mnd  18936  mulgpropd  19147  imasabl  19909  dprdss  20064  subrgdvds  20603  rhmsscrnghm  20682  dmatsubcl  22520  scmatcrng  22543  epttop  23032  cnprest  23313  lmmo  23404  lly1stc  23520  txcnp  23644  addcnlem  24900  clmvscom  25137  caussi  25345  bcthlem5  25376  ovollb2lem  25537  voliunlem1  25599  ioombl1lem4  25610  rolle  26043  c1lip1  26051  c1lip3  26053  ulmval  26438  sqf11  27197  fsumvma  27272  dchrelbas3  27297  nocvxminlem  27837  nocvxmin  27838  conway  27859  cofcut1  27969  precsexlem10  28255  acopy  28856  brbtwn2  28935  axeuclidlem  28992  axcontlem9  29002  axcontlem10  29003  umgrvad2edg  29245  upgrwlkdvdelem  29769  usgr2wlkneq  29789  2wlkdlem6  29961  umgr2adedgwlklem  29974  umgr2adedgspth  29978  2pthfrgrrn2  30312  frgrnbnb  30322  fusgr2wsp2nb  30363  nmcvcn  30724  sspmval  30762  sspimsval  30767  shsubcl  31249  shorth  31324  5oalem6  31688  strlem1  32279  atexch  32410  cdj3i  32470  xrofsup  32778  nnindf  32826  cnre2csqima  33872  nummin  35084  subgrwlk  35117  cusgr3cyclex  35121  erdszelem9  35184  erdsze2lem2  35189  gonarlem  35379  satffunlem  35386  satefvfmla1  35410  ss2mcls  35553  funpsstri  35747  dfon2lem4  35768  dfon2  35774  wsuclem  35807  elfuns  35897  btwnswapid  35999  ifscgr  36026  hilbert1.2  36137  elicc3  36300  tailfb  36360  bj-nnfand  36732  bj-gabss  36918  bj-imdirval3  37167  pibt2  37400  wl-mo3t  37557  ltflcei  37595  tan2h  37599  mblfinlem3  37646  fzmul  37728  metf1o  37742  ismtycnv  37789  ismtyres  37795  crngohomfo  37993  cossss  38407  funALTVss  38681  disjss  38713  hlhgt2  39372  hl2at  39388  2llnjN  39550  2lplnj  39603  linepsubN  39735  cdlemg33b0  40684  dvh3dim3N  41432  mapdh9a  41772  fltaccoprm  42627  iocinico  43201  clcnvlem  43613  ismnushort  44297  pm11.59  44387  f1cof1b  47027  afvres  47122  afv2res  47189  isuspgrim0lem  47809  isuspgrimlem  47812  ply1mulgsumlem1  48232  fldivexpfllog2  48415