Theorem anim12d 612

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anim12d1  613  anim1d  614  anim2d  615  anim12dan  622  3anim123d  1445  mo3  2563  mo4  2565  2euswapv  2631  2euswap  2646  disj  4362  ssunsn2  4740  prel12g  4774  disjiun  5040  soss  5488  wess  5538  frinxp  5631  trin2  5988  xp11  6038  oneqmini  6264  funss  6399  fvcofneq  6912  dff13  7067  f1cofveqaeq  7070  f1eqcocnv  7111  f1eqcocnvOLD  7112  isores3  7144  isosolem  7156  isowe2  7159  trom  7653  f1oweALT  7745  f1o2ndf1  7891  suppofssd  7945  tposfn2  7990  tposf1o2  7994  frrlem4  8030  wfrlem4  8058  smo11  8101  tz7.48lem  8177  om00  8303  omsmo  8383  ixpfi2  8974  elfiun  9046  supmo  9068  infmo  9111  trpredrec  9342  frmin  9365  cardaleph  9703  dfac5  9742  fin1a2lem9  10022  axdc3lem2  10065  zorn2lem6  10115  indpi  10521  genpnmax  10621  reclem3pr  10663  reclem4pr  10664  suplem1pr  10666  supsrlem  10725  dedekind  10995  lemul12b  11689  lbreu  11782  supadd  11800  supmullem2  11803  cju  11826  nnind  11848  uz11  12463  xrre2  12760  qbtwnre  12789  ico0  12981  ioc0  12982  ssfzoulel  13336  ishashinf  14029  swrdccatin2  14294  coss12d  14535  sqrlem6  14811  o1lo1  15098  ruclem9  15799  isprm3  16240  eulerthlem2  16335  prmdiveq  16339  ramub2  16567  cictr  17310  clatl  18014  lubun  18021  ipodrsima  18047  dirtr  18108  smndex1mgm  18334  smndex1sgrp  18335  smndex1mnd  18337  mulgpropd  18533  dprdss  19416  subrgdvds  19814  dmatsubcl  21395  scmatcrng  21418  epttop  21906  cnprest  22186  lmmo  22277  lly1stc  22393  txcnp  22517  addcnlem  23761  clmvscom  23987  caussi  24194  bcthlem5  24225  ovollb2lem  24385  voliunlem1  24447  ioombl1lem4  24458  rolle  24887  c1lip1  24894  c1lip3  24896  ulmval  25272  sqf11  26021  fsumvma  26094  dchrelbas3  26119  acopy  26924  brbtwn2  26996  axeuclidlem  27053  axcontlem9  27063  axcontlem10  27064  umgrvad2edg  27301  upgrwlkdvdelem  27823  usgr2wlkneq  27843  2wlkdlem6  28015  umgr2adedgwlklem  28028  umgr2adedgspth  28032  2pthfrgrrn2  28366  frgrnbnb  28376  fusgr2wsp2nb  28417  nmcvcn  28776  sspmval  28814  sspimsval  28819  shsubcl  29301  shorth  29376  5oalem6  29740  strlem1  30331  atexch  30462  cdj3i  30522  xrofsup  30810  nnindf  30853  cnre2csqima  31575  nummin  32776  subgrwlk  32807  cusgr3cyclex  32811  erdszelem9  32874  erdsze2lem2  32879  gonarlem  33069  satffunlem  33076  satefvfmla1  33100  ss2mcls  33243  funpsstri  33458  dfon2lem4  33481  dfon2  33487  wsuclem  33556  nocvxminlem  33709  nocvxmin  33710  conway  33730  cofcut1  33827  elfuns  33954  btwnswapid  34056  ifscgr  34083  hilbert1.2  34194  elicc3  34243  tailfb  34303  bj-nnfand  34668  bj-gabss  34860  bj-imdirval3  35090  pibt2  35325  wl-mo3t  35468  ltflcei  35502  tan2h  35506  mblfinlem3  35553  fzmul  35636  metf1o  35650  ismtycnv  35697  ismtyres  35703  crngohomfo  35901  cossss  36285  funALTVss  36547  disjss  36579  hlhgt2  37140  hl2at  37156  2llnjN  37318  2lplnj  37371  linepsubN  37503  cdlemg33b0  38452  dvh3dim3N  39200  mapdh9a  39540  fltaccoprm  40180  iocinico  40746  clcnvlem  40907  ismnushort  41592  pm11.59  41682  f1cof1b  44241  afvres  44336  afv2res  44403  isomuspgrlem1  44952  isomuspgrlem2c  44955  isomuspgrlem2d  44956  rhmsscrnghm  45257  ply1mulgsumlem1  45400  fldivexpfllog2  45584