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  2557  2euswapv  2623  2euswap  2638  disj  4403  ssunsn2  4781  prel12g  4818  disjiun  5083  soss  5551  wess  5609  frinxp  5706  trin2  6076  xp11  6128  oneqmini  6364  funss  6505  fvcofneq  7031  dff13  7195  f1cofveqaeq  7198  f1eqcocnv  7242  isores3  7276  isosolem  7288  isowe2  7291  trom  7815  f1oweALT  7914  f1o2ndf1  8062  suppofssd  8143  tposfn2  8188  tposf1o2  8192  frrlem4  8229  smo11  8294  tz7.48lem  8370  om00  8500  omsmo  8583  ixpfi2  9259  elfiun  9339  supmo  9361  infmo  9406  frmin  9664  cardaleph  10002  dfac5  10042  fin1a2lem9  10321  axdc3lem2  10364  zorn2lem6  10414  indpi  10820  genpnmax  10920  reclem3pr  10962  reclem4pr  10963  suplem1pr  10965  supsrlem  11024  dedekind  11297  lemul12b  11999  lbreu  12093  supadd  12111  supmullem2  12114  cju  12142  nnind  12164  uz11  12778  xrre2  13090  qbtwnre  13119  ico0  13312  ioc0  13313  ssfzoulel  13681  ishashinf  14388  swrdccatin2  14653  coss12d  14897  01sqrexlem6  15172  o1lo1  15462  ruclem9  16165  isprm3  16612  eulerthlem2  16711  prmdiveq  16715  ramub2  16944  cictr  17730  clatl  18432  lubun  18439  ipodrsima  18465  dirtr  18526  smndex1mgm  18799  smndex1sgrp  18800  smndex1mnd  18802  mulgpropd  19013  imasabl  19773  dprdss  19928  subrgdvds  20489  rhmsscrnghm  20568  dmatsubcl  22401  scmatcrng  22424  epttop  22912  cnprest  23192  lmmo  23283  lly1stc  23399  txcnp  23523  addcnlem  24769  clmvscom  25006  caussi  25213  bcthlem5  25244  ovollb2lem  25405  voliunlem1  25467  ioombl1lem4  25478  rolle  25910  c1lip1  25918  c1lip3  25920  ulmval  26305  sqf11  27065  fsumvma  27140  dchrelbas3  27165  nocvxminlem  27706  nocvxmin  27707  conway  27728  cofcut1  27851  precsexlem10  28141  acopy  28796  brbtwn2  28868  axeuclidlem  28925  axcontlem9  28935  axcontlem10  28936  umgrvad2edg  29176  upgrwlkdvdelem  29699  usgr2wlkneq  29719  2wlkdlem6  29894  umgr2adedgwlklem  29907  umgr2adedgspth  29911  2pthfrgrrn2  30245  frgrnbnb  30255  fusgr2wsp2nb  30296  nmcvcn  30657  sspmval  30695  sspimsval  30700  shsubcl  31182  shorth  31257  5oalem6  31621  strlem1  32212  atexch  32343  cdj3i  32403  xrofsup  32723  nnindf  32777  cnre2csqima  33877  nummin  35057  subgrwlk  35104  cusgr3cyclex  35108  erdszelem9  35171  erdsze2lem2  35176  gonarlem  35366  satffunlem  35373  satefvfmla1  35397  ss2mcls  35540  funpsstri  35738  dfon2lem4  35759  dfon2  35765  wsuclem  35798  elfuns  35888  btwnswapid  35990  ifscgr  36017  hilbert1.2  36128  elicc3  36290  tailfb  36350  bj-nnfand  36722  bj-gabss  36908  bj-imdirval3  37157  pibt2  37390  wl-mo3t  37549  ltflcei  37587  tan2h  37591  mblfinlem3  37638  fzmul  37720  metf1o  37734  ismtycnv  37781  ismtyres  37787  crngohomfo  37985  cossss  38401  funALTVss  38676  disjss  38708  hlhgt2  39368  hl2at  39384  2llnjN  39546  2lplnj  39599  linepsubN  39731  cdlemg33b0  40680  dvh3dim3N  41428  mapdh9a  41768  fltaccoprm  42613  iocinico  43185  clcnvlem  43596  ismnushort  44274  pm11.59  44364  f1cof1b  47062  afvres  47157  afv2res  47224  isuspgrim0lem  47877  isuspgrimlem  47879  ply1mulgsumlem1  48359  fldivexpfllog2  48538