Theorem anim12d 587

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  anim12d1  588  anim1d  589  anim2d  590  prth  596  im2anan9  916  anim12dan  918  3anim123d  1555  mo3  2645  2euswap  2686  ssunsn2  4504  prel12g  4544  disjiun  4792  soss  5205  wess  5253  frinxp  5341  trin2  5677  xp11  5727  ordtri3OLD  5921  oneqmini  5937  funss  6068  fun  6227  fvcofneq  6530  dff13  6675  f1cofveqaeq  6678  f1eqcocnv  6719  isores3  6748  isosolem  6760  isowe2  6763  ordom  7239  f1oweALT  7317  f1o2ndf1  7453  tposfn2  7543  tposf1o2  7547  wfrlem4  7587  smo11  7630  tz7.48lem  7705  om00  7824  omsmo  7903  ixpfi2  8429  elfiun  8501  supmo  8523  infmo  8566  alephord  9088  cardaleph  9102  dfac5  9141  fin1a2lem9  9422  axdc3lem2  9465  zorn2lem6  9515  grudomon  9831  indpi  9921  genpnmax  10021  reclem3pr  10063  reclem4pr  10064  suplem1pr  10066  supsrlem  10124  dedekind  10392  lemul12b  11072  fimaxre  11160  lbreu  11165  supadd  11183  supmullem2  11186  cju  11208  nnind  11230  uz11  11902  xrre2  12194  qbtwnre  12223  xrsupexmnf  12328  xrinfmexpnf  12329  ico0  12414  ioc0  12415  ssfzoulel  12756  ishashinf  13439  swrdccatin2  13687  coss12d  13912  sqrlem6  14187  o1lo1  14467  ruclem9  15166  isprm3  15598  eulerthlem2  15689  prmdiveq  15693  ramub2  15920  cictr  16666  joinfval  17202  meetfval  17216  clatl  17317  lubun  17324  ipodrsima  17366  dirtr  17437  mulgpropd  17785  dprdss  18628  subrgdvds  18996  dmatsubcl  20506  scmatcrng  20529  epttop  21015  cnpresti  21294  cnprest  21295  lmmo  21386  1stcrest  21458  lly1stc  21501  txcnp  21625  addcnlem  22868  clmvscom  23090  caussi  23295  bcthlem5  23325  ovollb2lem  23456  voliunlem1  23518  ioombl1lem4  23529  rolle  23952  c1lip1  23959  c1lip3  23961  ulmval  24333  sqf11  25064  fsumvma  25137  dchrelbas3  25162  acopy  25923  brbtwn2  25984  axeuclidlem  26041  axcontlem9  26051  axcontlem10  26052  umgrvad2edg  26304  upgrwlkdvdelem  26842  usgr2wlkneq  26862  2wlkdlem6  27051  umgr2adedgwlklem  27064  umgr2adedgspth  27068  2pthfrgrrn2  27437  frgrnbnb  27447  fusgr2wsp2nb  27488  nmcvcn  27859  sspmval  27897  sspimsval  27902  sspph  28019  shsubcl  28386  shorth  28463  5oalem6  28827  strlem1  29418  atexch  29549  cdj3i  29609  xrofsup  29842  nnindf  29874  cnre2csqima  30266  erdszelem9  31488  erdsze2lem2  31493  ss2mcls  31772  funpsstri  31970  dfon2lem4  31996  dfon2  32002  trpredrec  32043  frmin  32048  wsuclem  32076  frrlem4  32089  nocvxminlem  32199  nocvxmin  32200  conway  32216  elfuns  32328  btwnswapid  32430  ifscgr  32457  hilbert1.2  32568  elicc3  32617  tailfb  32678  wl-mo3t  33671  ltflcei  33710  tan2h  33714  mblfinlem3  33761  fzmul  33850  metf1o  33864  ismtycnv  33914  ismtyres  33920  crngohomfo  34118  cossss  34503  hlhgt2  35178  hl2at  35194  2llnjN  35356  2lplnj  35409  linepsubN  35541  cdlemg33b0  36491  dvh3dim3N  37240  mapdh9a  37581  iocinico  38299  clcnvlem  38432  pm11.59  39093  afvres  41758  rhmsscrnghm  42536  ply1mulgsumlem1  42684  fldivexpfllog2  42869