Theorem anim12d 607

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  anim12d1  608  anim1d  609  anim2d  610  anim12dan  617  3anim123d  1439  mo3  2552  mo4  2554  2euswapv  2618  2euswap  2633  disj  4451  ssunsn2  4835  prel12g  4869  disjiun  5139  soss  5613  wess  5668  frinxp  5763  trin2  6134  xp11  6185  oneqmini  6427  funss  6577  fvcofneq  7106  dff13  7269  f1cofveqaeq  7272  f1eqcocnv  7314  isores3  7346  isosolem  7358  isowe2  7361  trom  7884  f1oweALT  7985  f1o2ndf1  8135  suppofssd  8217  tposfn2  8262  tposf1o2  8266  frrlem4  8303  wfrlem4OLD  8341  smo11  8393  tz7.48lem  8470  om00  8604  omsmo  8687  ixpfi2  9390  elfiun  9469  supmo  9491  infmo  9534  frmin  9788  cardaleph  10128  dfac5  10167  fin1a2lem9  10447  axdc3lem2  10490  zorn2lem6  10540  indpi  10946  genpnmax  11046  reclem3pr  11088  reclem4pr  11089  suplem1pr  11091  supsrlem  11150  dedekind  11423  lemul12b  12118  lbreu  12211  supadd  12229  supmullem2  12232  cju  12255  nnind  12277  uz11  12894  xrre2  13198  qbtwnre  13227  ico0  13419  ioc0  13420  ssfzoulel  13775  ishashinf  14477  swrdccatin2  14732  coss12d  14972  01sqrexlem6  15247  o1lo1  15534  ruclem9  16235  isprm3  16679  eulerthlem2  16779  prmdiveq  16783  ramub2  17011  cictr  17816  clatl  18528  lubun  18535  ipodrsima  18561  dirtr  18622  smndex1mgm  18892  smndex1sgrp  18893  smndex1mnd  18895  mulgpropd  19105  imasabl  19869  dprdss  20024  subrgdvds  20565  rhmsscrnghm  20638  dmatsubcl  22483  scmatcrng  22506  epttop  22995  cnprest  23276  lmmo  23367  lly1stc  23483  txcnp  23607  addcnlem  24863  clmvscom  25100  caussi  25308  bcthlem5  25339  ovollb2lem  25500  voliunlem1  25562  ioombl1lem4  25573  rolle  26005  c1lip1  26013  c1lip3  26015  ulmval  26401  sqf11  27159  fsumvma  27234  dchrelbas3  27259  nocvxminlem  27799  nocvxmin  27800  conway  27821  cofcut1  27929  precsexlem10  28207  acopy  28752  brbtwn2  28831  axeuclidlem  28888  axcontlem9  28898  axcontlem10  28899  umgrvad2edg  29141  upgrwlkdvdelem  29665  usgr2wlkneq  29685  2wlkdlem6  29857  umgr2adedgwlklem  29870  umgr2adedgspth  29874  2pthfrgrrn2  30208  frgrnbnb  30218  fusgr2wsp2nb  30259  nmcvcn  30620  sspmval  30658  sspimsval  30663  shsubcl  31145  shorth  31220  5oalem6  31584  strlem1  32175  atexch  32306  cdj3i  32366  xrofsup  32660  nnindf  32709  cnre2csqima  33694  nummin  34896  subgrwlk  34924  cusgr3cyclex  34928  erdszelem9  34991  erdsze2lem2  34996  gonarlem  35186  satffunlem  35193  satefvfmla1  35217  ss2mcls  35360  funpsstri  35549  dfon2lem4  35570  dfon2  35576  wsuclem  35609  elfuns  35699  btwnswapid  35801  ifscgr  35828  hilbert1.2  35939  elicc3  35989  tailfb  36049  bj-nnfand  36414  bj-gabss  36601  bj-imdirval3  36851  pibt2  37084  wl-mo3t  37231  ltflcei  37269  tan2h  37273  mblfinlem3  37320  fzmul  37402  metf1o  37416  ismtycnv  37463  ismtyres  37469  crngohomfo  37667  cossss  38083  funALTVss  38357  disjss  38389  hlhgt2  39048  hl2at  39064  2llnjN  39226  2lplnj  39279  linepsubN  39411  cdlemg33b0  40360  dvh3dim3N  41108  mapdh9a  41448  fltaccoprm  42243  iocinico  42826  clcnvlem  43239  ismnushort  43924  pm11.59  44014  f1cof1b  46639  afvres  46734  afv2res  46801  isuspgrim0lem  47399  isuspgrimlem  47402  ply1mulgsumlem1  47718  fldivexpfllog2  47902