Theorem anim12d 610

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 609	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  611  anim1d  612  anim2d  613  anim12dan  620  3anim123d  1446  mo3  2565  2euswapv  2631  2euswap  2646  ssunsn2  4771  prel12g  4808  disjiun  5074  soss  5552  wess  5610  frinxp  5707  trin2  6080  xp11  6133  oneqmini  6370  funss  6511  fvcofneq  7039  dff13  7202  f1cofveqaeq  7205  f1eqcocnv  7249  isores3  7283  isosolem  7295  isowe2  7298  trom  7819  f1oweALT  7918  f1o2ndf1  8065  suppofssd  8146  tposfn2  8191  tposf1o2  8195  frrlem4  8232  smo11  8297  tz7.48lem  8373  om00  8503  omsmo  8587  ixpfi2  9253  elfiun  9336  supmo  9358  infmo  9403  frmin  9664  cardaleph  10002  dfac5  10042  fin1a2lem9  10321  axdc3lem2  10364  zorn2lem6  10414  indpi  10821  genpnmax  10921  reclem3pr  10963  reclem4pr  10964  suplem1pr  10966  supsrlem  11025  dedekind  11300  lemul12b  12003  lbreu  12097  supadd  12115  supmullem2  12118  cju  12146  nnind  12183  uz11  12804  xrre2  13113  qbtwnre  13142  ico0  13335  ioc0  13336  ssfzoulel  13706  ishashinf  14416  swrdccatin2  14682  coss12d  14925  01sqrexlem6  15200  o1lo1  15490  ruclem9  16196  isprm3  16643  eulerthlem2  16743  prmdiveq  16747  ramub2  16976  cictr  17763  clatl  18465  lubun  18472  ipodrsima  18498  dirtr  18559  smndex1mgm  18869  smndex1sgrp  18870  smndex1mnd  18872  mulgpropd  19083  imasabl  19842  dprdss  19997  subrgdvds  20554  rhmsscrnghm  20633  dmatsubcl  22473  scmatcrng  22496  epttop  22984  cnprest  23264  lmmo  23355  lly1stc  23471  txcnp  23595  addcnlem  24840  clmvscom  25067  caussi  25274  bcthlem5  25305  ovollb2lem  25465  voliunlem1  25527  ioombl1lem4  25538  rolle  25967  c1lip1  25974  c1lip3  25976  ulmval  26358  sqf11  27116  fsumvma  27190  dchrelbas3  27215  nocvxminlem  27760  nocvxmin  27761  conway  27785  cofcut1  27926  precsexlem10  28222  acopy  28915  brbtwn2  28988  axeuclidlem  29045  axcontlem9  29055  axcontlem10  29056  umgrvad2edg  29296  upgrwlkdvdelem  29819  usgr2wlkneq  29839  2wlkdlem6  30014  umgr2adedgwlklem  30027  umgr2adedgspth  30031  2pthfrgrrn2  30368  frgrnbnb  30378  fusgr2wsp2nb  30419  nmcvcn  30781  sspmval  30819  sspimsval  30824  shsubcl  31306  shorth  31381  5oalem6  31745  strlem1  32336  atexch  32467  cdj3i  32527  xrofsup  32855  nnindf  32908  cnre2csqima  34071  nummin  35252  subgrwlk  35330  cusgr3cyclex  35334  erdszelem9  35397  erdsze2lem2  35402  gonarlem  35592  satffunlem  35599  satefvfmla1  35623  ss2mcls  35766  funpsstri  35964  dfon2lem4  35982  dfon2  35988  wsuclem  36021  elfuns  36111  btwnswapid  36215  ifscgr  36242  hilbert1.2  36353  elicc3  36515  tailfb  36575  dfttc4lem2  36727  bj-nnfand  37068  bj-gabss  37258  bj-imdirval3  37514  pibt2  37747  wl-mo3t  37915  ltflcei  37943  tan2h  37947  mblfinlem3  37994  fzmul  38076  metf1o  38090  ismtycnv  38137  ismtyres  38143  crngohomfo  38341  cossss  38850  funALTVss  39119  disjss  39166  hlhgt2  39849  hl2at  39865  2llnjN  40027  2lplnj  40080  linepsubN  40212  cdlemg33b0  41161  dvh3dim3N  41909  mapdh9a  42249  fltaccoprm  43087  iocinico  43658  clcnvlem  44068  ismnushort  44746  pm11.59  44836  f1cof1b  47537  afvres  47632  afv2res  47699  isuspgrim0lem  48381  isuspgrimlem  48383  grlimprclnbgrvtx  48487  ply1mulgsumlem1  48874  fldivexpfllog2  49053