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  1445  mo3  2558  2euswapv  2624  2euswap  2639  disj  4416  ssunsn2  4794  prel12g  4831  disjiun  5098  soss  5569  wess  5627  frinxp  5724  trin2  6099  xp11  6151  oneqmini  6388  funss  6538  fvcofneq  7068  dff13  7232  f1cofveqaeq  7235  f1eqcocnv  7279  isores3  7313  isosolem  7325  isowe2  7328  trom  7854  f1oweALT  7954  f1o2ndf1  8104  suppofssd  8185  tposfn2  8230  tposf1o2  8234  frrlem4  8271  smo11  8336  tz7.48lem  8412  om00  8542  omsmo  8625  ixpfi2  9308  elfiun  9388  supmo  9410  infmo  9455  frmin  9709  cardaleph  10049  dfac5  10089  fin1a2lem9  10368  axdc3lem2  10411  zorn2lem6  10461  indpi  10867  genpnmax  10967  reclem3pr  11009  reclem4pr  11010  suplem1pr  11012  supsrlem  11071  dedekind  11344  lemul12b  12046  lbreu  12140  supadd  12158  supmullem2  12161  cju  12189  nnind  12211  uz11  12825  xrre2  13137  qbtwnre  13166  ico0  13359  ioc0  13360  ssfzoulel  13728  ishashinf  14435  swrdccatin2  14701  coss12d  14945  01sqrexlem6  15220  o1lo1  15510  ruclem9  16213  isprm3  16660  eulerthlem2  16759  prmdiveq  16763  ramub2  16992  cictr  17774  clatl  18474  lubun  18481  ipodrsima  18507  dirtr  18568  smndex1mgm  18841  smndex1sgrp  18842  smndex1mnd  18844  mulgpropd  19055  imasabl  19813  dprdss  19968  subrgdvds  20502  rhmsscrnghm  20581  dmatsubcl  22392  scmatcrng  22415  epttop  22903  cnprest  23183  lmmo  23274  lly1stc  23390  txcnp  23514  addcnlem  24760  clmvscom  24997  caussi  25204  bcthlem5  25235  ovollb2lem  25396  voliunlem1  25458  ioombl1lem4  25469  rolle  25901  c1lip1  25909  c1lip3  25911  ulmval  26296  sqf11  27056  fsumvma  27131  dchrelbas3  27156  nocvxminlem  27696  nocvxmin  27697  conway  27718  cofcut1  27835  precsexlem10  28125  acopy  28767  brbtwn2  28839  axeuclidlem  28896  axcontlem9  28906  axcontlem10  28907  umgrvad2edg  29147  upgrwlkdvdelem  29673  usgr2wlkneq  29693  2wlkdlem6  29868  umgr2adedgwlklem  29881  umgr2adedgspth  29885  2pthfrgrrn2  30219  frgrnbnb  30229  fusgr2wsp2nb  30270  nmcvcn  30631  sspmval  30669  sspimsval  30674  shsubcl  31156  shorth  31231  5oalem6  31595  strlem1  32186  atexch  32317  cdj3i  32377  xrofsup  32697  nnindf  32751  cnre2csqima  33908  nummin  35088  subgrwlk  35126  cusgr3cyclex  35130  erdszelem9  35193  erdsze2lem2  35198  gonarlem  35388  satffunlem  35395  satefvfmla1  35419  ss2mcls  35562  funpsstri  35760  dfon2lem4  35781  dfon2  35787  wsuclem  35820  elfuns  35910  btwnswapid  36012  ifscgr  36039  hilbert1.2  36150  elicc3  36312  tailfb  36372  bj-nnfand  36744  bj-gabss  36930  bj-imdirval3  37179  pibt2  37412  wl-mo3t  37571  ltflcei  37609  tan2h  37613  mblfinlem3  37660  fzmul  37742  metf1o  37756  ismtycnv  37803  ismtyres  37809  crngohomfo  38007  cossss  38423  funALTVss  38698  disjss  38730  hlhgt2  39390  hl2at  39406  2llnjN  39568  2lplnj  39621  linepsubN  39753  cdlemg33b0  40702  dvh3dim3N  41450  mapdh9a  41790  fltaccoprm  42635  iocinico  43208  clcnvlem  43619  ismnushort  44297  pm11.59  44387  f1cof1b  47082  afvres  47177  afv2res  47244  isuspgrim0lem  47897  isuspgrimlem  47899  ply1mulgsumlem1  48379  fldivexpfllog2  48558