Theorem anim12d 608

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 607	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  609  anim1d  610  anim2d  611  anim12dan  618  3anim123d  1443  mo3  2567  mo4  2569  2euswapv  2633  2euswap  2648  disj  4473  ssunsn2  4852  prel12g  4888  disjiun  5154  soss  5628  wess  5686  frinxp  5782  trin2  6155  xp11  6206  oneqmini  6447  funss  6597  fvcofneq  7127  dff13  7292  f1cofveqaeq  7295  f1eqcocnv  7337  isores3  7371  isosolem  7383  isowe2  7386  trom  7912  f1oweALT  8013  f1o2ndf1  8163  suppofssd  8244  tposfn2  8289  tposf1o2  8293  frrlem4  8330  wfrlem4OLD  8368  smo11  8420  tz7.48lem  8497  om00  8631  omsmo  8714  ixpfi2  9420  elfiun  9499  supmo  9521  infmo  9564  frmin  9818  cardaleph  10158  dfac5  10198  fin1a2lem9  10477  axdc3lem2  10520  zorn2lem6  10570  indpi  10976  genpnmax  11076  reclem3pr  11118  reclem4pr  11119  suplem1pr  11121  supsrlem  11180  dedekind  11453  lemul12b  12151  lbreu  12245  supadd  12263  supmullem2  12266  cju  12289  nnind  12311  uz11  12928  xrre2  13232  qbtwnre  13261  ico0  13453  ioc0  13454  ssfzoulel  13810  ishashinf  14512  swrdccatin2  14777  coss12d  15021  01sqrexlem6  15296  o1lo1  15583  ruclem9  16286  isprm3  16730  eulerthlem2  16829  prmdiveq  16833  ramub2  17061  cictr  17866  clatl  18578  lubun  18585  ipodrsima  18611  dirtr  18672  smndex1mgm  18942  smndex1sgrp  18943  smndex1mnd  18945  mulgpropd  19156  imasabl  19918  dprdss  20073  subrgdvds  20614  rhmsscrnghm  20687  dmatsubcl  22525  scmatcrng  22548  epttop  23037  cnprest  23318  lmmo  23409  lly1stc  23525  txcnp  23649  addcnlem  24905  clmvscom  25142  caussi  25350  bcthlem5  25381  ovollb2lem  25542  voliunlem1  25604  ioombl1lem4  25615  rolle  26048  c1lip1  26056  c1lip3  26058  ulmval  26441  sqf11  27200  fsumvma  27275  dchrelbas3  27300  nocvxminlem  27840  nocvxmin  27841  conway  27862  cofcut1  27972  precsexlem10  28258  acopy  28859  brbtwn2  28938  axeuclidlem  28995  axcontlem9  29005  axcontlem10  29006  umgrvad2edg  29248  upgrwlkdvdelem  29772  usgr2wlkneq  29792  2wlkdlem6  29964  umgr2adedgwlklem  29977  umgr2adedgspth  29981  2pthfrgrrn2  30315  frgrnbnb  30325  fusgr2wsp2nb  30366  nmcvcn  30727  sspmval  30765  sspimsval  30770  shsubcl  31252  shorth  31327  5oalem6  31691  strlem1  32282  atexch  32413  cdj3i  32473  xrofsup  32774  nnindf  32823  cnre2csqima  33857  nummin  35067  subgrwlk  35100  cusgr3cyclex  35104  erdszelem9  35167  erdsze2lem2  35172  gonarlem  35362  satffunlem  35369  satefvfmla1  35393  ss2mcls  35536  funpsstri  35729  dfon2lem4  35750  dfon2  35756  wsuclem  35789  elfuns  35879  btwnswapid  35981  ifscgr  36008  hilbert1.2  36119  elicc3  36283  tailfb  36343  bj-nnfand  36715  bj-gabss  36901  bj-imdirval3  37150  pibt2  37383  wl-mo3t  37530  ltflcei  37568  tan2h  37572  mblfinlem3  37619  fzmul  37701  metf1o  37715  ismtycnv  37762  ismtyres  37768  crngohomfo  37966  cossss  38381  funALTVss  38655  disjss  38687  hlhgt2  39346  hl2at  39362  2llnjN  39524  2lplnj  39577  linepsubN  39709  cdlemg33b0  40658  dvh3dim3N  41406  mapdh9a  41746  fltaccoprm  42595  iocinico  43173  clcnvlem  43585  ismnushort  44270  pm11.59  44360  f1cof1b  46992  afvres  47087  afv2res  47154  isuspgrim0lem  47755  isuspgrimlem  47758  ply1mulgsumlem1  48115  fldivexpfllog2  48299