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  1444  mo3  2563  mo4  2565  2euswapv  2629  2euswap  2644  disj  4449  ssunsn2  4826  prel12g  4863  disjiun  5130  soss  5611  wess  5670  frinxp  5767  trin2  6142  xp11  6194  oneqmini  6435  funss  6584  fvcofneq  7112  dff13  7276  f1cofveqaeq  7279  f1eqcocnv  7322  isores3  7356  isosolem  7368  isowe2  7371  trom  7897  f1oweALT  7998  f1o2ndf1  8148  suppofssd  8229  tposfn2  8274  tposf1o2  8278  frrlem4  8315  wfrlem4OLD  8353  smo11  8405  tz7.48lem  8482  om00  8614  omsmo  8697  ixpfi2  9391  elfiun  9471  supmo  9493  infmo  9536  frmin  9790  cardaleph  10130  dfac5  10170  fin1a2lem9  10449  axdc3lem2  10492  zorn2lem6  10542  indpi  10948  genpnmax  11048  reclem3pr  11090  reclem4pr  11091  suplem1pr  11093  supsrlem  11152  dedekind  11425  lemul12b  12125  lbreu  12219  supadd  12237  supmullem2  12240  cju  12263  nnind  12285  uz11  12904  xrre2  13213  qbtwnre  13242  ico0  13434  ioc0  13435  ssfzoulel  13800  ishashinf  14503  swrdccatin2  14768  coss12d  15012  01sqrexlem6  15287  o1lo1  15574  ruclem9  16275  isprm3  16721  eulerthlem2  16820  prmdiveq  16824  ramub2  17053  cictr  17850  clatl  18554  lubun  18561  ipodrsima  18587  dirtr  18648  smndex1mgm  18921  smndex1sgrp  18922  smndex1mnd  18924  mulgpropd  19135  imasabl  19895  dprdss  20050  subrgdvds  20587  rhmsscrnghm  20666  dmatsubcl  22505  scmatcrng  22528  epttop  23017  cnprest  23298  lmmo  23389  lly1stc  23505  txcnp  23629  addcnlem  24887  clmvscom  25124  caussi  25332  bcthlem5  25363  ovollb2lem  25524  voliunlem1  25586  ioombl1lem4  25597  rolle  26029  c1lip1  26037  c1lip3  26039  ulmval  26424  sqf11  27183  fsumvma  27258  dchrelbas3  27283  nocvxminlem  27823  nocvxmin  27824  conway  27845  cofcut1  27955  precsexlem10  28241  acopy  28842  brbtwn2  28921  axeuclidlem  28978  axcontlem9  28988  axcontlem10  28989  umgrvad2edg  29231  upgrwlkdvdelem  29757  usgr2wlkneq  29777  2wlkdlem6  29952  umgr2adedgwlklem  29965  umgr2adedgspth  29969  2pthfrgrrn2  30303  frgrnbnb  30313  fusgr2wsp2nb  30354  nmcvcn  30715  sspmval  30753  sspimsval  30758  shsubcl  31240  shorth  31315  5oalem6  31679  strlem1  32270  atexch  32401  cdj3i  32461  xrofsup  32772  nnindf  32822  cnre2csqima  33911  nummin  35106  subgrwlk  35138  cusgr3cyclex  35142  erdszelem9  35205  erdsze2lem2  35210  gonarlem  35400  satffunlem  35407  satefvfmla1  35431  ss2mcls  35574  funpsstri  35767  dfon2lem4  35788  dfon2  35794  wsuclem  35827  elfuns  35917  btwnswapid  36019  ifscgr  36046  hilbert1.2  36157  elicc3  36319  tailfb  36379  bj-nnfand  36751  bj-gabss  36937  bj-imdirval3  37186  pibt2  37419  wl-mo3t  37578  ltflcei  37616  tan2h  37620  mblfinlem3  37667  fzmul  37749  metf1o  37763  ismtycnv  37810  ismtyres  37816  crngohomfo  38014  cossss  38427  funALTVss  38701  disjss  38733  hlhgt2  39392  hl2at  39408  2llnjN  39570  2lplnj  39623  linepsubN  39755  cdlemg33b0  40704  dvh3dim3N  41452  mapdh9a  41792  fltaccoprm  42655  iocinico  43229  clcnvlem  43641  ismnushort  44325  pm11.59  44415  f1cof1b  47094  afvres  47189  afv2res  47256  isuspgrim0lem  47876  isuspgrimlem  47879  ply1mulgsumlem1  48308  fldivexpfllog2  48491