Theorem anim12d 621

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 25	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → (𝜒 ∧ 𝜏)))
4	1, 2, 3	syl2and 620	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anim12d1  622  anim1d  623  anim2d  624  anim12dan  631  3anim123d  1471  mo3  2589  2euswapv  2655  2euswap  2670  ssunsn2  4787  prel12g  4823  disjiun  5090  soss  5578  wess  5636  frinxp  5733  trin2  6116  xp11  6166  oneqmini  6416  funss  6558  fvcofneq  7093  dff13  7258  f1cofveqaeq  7261  f1eqcocnv  7309  isores3  7343  isosolem  7355  isowe2  7358  trom  7886  f1oweALT  7984  f1o2ndf1  8133  suppofssd  8221  tposfn2  8266  tposf1o2  8270  frrlem4  8308  smo11  8373  tz7.48lemOLD  8452  om00  8584  omsmo  8668  ixpfi2  9340  elfiun  9423  supmo  9445  infmo  9490  frmin  9754  cardaleph  10169  dfac5  10208  fin1a2lem9  10487  axdc3lem2  10530  zorn2lem6  10580  indpi  10993  genpnmax  11093  reclem3pr  11135  reclem4pr  11136  suplem1pr  11138  supsrlem  11197  dedekind  11474  lemul12b  12175  lbreu  12268  supadd  12286  supmullem2  12289  cju  12317  nnind  12354  uz11  12991  xrre2  13301  qbtwnre  13330  ico0  13523  ioc0  13524  ssfzoulel  13896  ishashinf  14609  swrdccatin2  14879  coss12d  15126  01sqrexlem6  15415  o1lo1  15705  ruclem9  16407  isprm3  16859  eulerthlem2  16960  prmdiveq  16964  ramub2  17193  cictr  17981  clatl  18683  lubun  18690  ipodrsima  18716  dirtr  18777  smndex1mgm  19107  smndex1sgrp  19108  smndex1mnd  19110  mulgpropd  19327  imasabl  20091  dprdss  20246  crngrhmfo  20727  subrgdvds  20839  rhmsscrnghm  20918  dmatsubcl  22814  scmatcrng  22837  epttop  23328  cnprest  23608  lmmo  23699  lly1stc  23816  txcnp  23940  addcnlem  25185  clmvscom  25412  caussi  25619  bcthlem5  25650  ovollb2lem  25810  voliunlem1  25872  ioombl1lem4  25883  rolle  26311  c1lip1  26318  c1lip3  26320  ulmval  26708  sqf11  27467  fsumvma  27541  dchrelbas3  27566  fltaccoprm  27973  nocvxminlem  28141  nocvxmin  28142  conway  28166  cofcut1  28307  precsexlem10  28603  acopy  29342  brbtwn2  29484  axeuclidlem  29541  axcontlem9  29551  axcontlem10  29552  umgrvad2edg  29795  subgrwlk  30270  upgrwlkdvdelem  30323  usgr2wlkneq  30343  2wlkdlem6  30521  umgr2adedgwlklem  30534  umgr2adedgspth  30538  2pthfrgrrn2  30885  frgrnbnb  30895  fusgr2wsp2nb  30936  nmcvcn  31298  sspmval  31336  sspimsval  31341  shsubcl  31823  shorth  31898  5oalem6  32262  strlem1  32853  atexch  32984  cdj3i  33044  xrofsup  33402  nnindf  33454  cnre2csqima  34586  nummin  35767  ackardcard  35884  cusgr3cyclex  35980  erdszelem9  36033  erdsze2lem2  36038  gonarlem  36228  satffunlem  36235  satefvfmla1  36259  ss2mcls  36402  funpsstri  36606  dfon2lem4  36623  dfon2  36629  wsuclem  36662  elfuns  36752  btwnswapid  36857  ifscgr  36884  hilbert1.2  36995  elicc3  37180  tailfb  37240  dfttc4lem2  37392  bj-nnfand  37732  bj-gabss  37923  bj-imdirval3  38181  pibt2  38416  wl-mo3t  38584  ltflcei  38607  tan2h  38611  mblfinlem3  38653  fzmul  38751  metf1o  38765  ismtycnv  38812  ismtyres  38818  crngohomfo  39016  cossss  39523  funALTVss  39792  disjss  39839  hlhgt2  40522  hl2at  40538  2llnjN  40700  2lplnj  40753  linepsubN  40885  cdlemg33b0  41834  dvh3dim3N  42582  mapdh9a  42922  iocinico  44290  clcnvlem  44699  ismnushort  45361  pm11.59  45451  f1cof1b  48223  afvres  48318  afv2res  48385  isuspgrim0lem  49067  isuspgrimlem  49069  grlimprclnbgrvtx  49173  ply1mulgsumlem1  49574  fldivexpfllog2  49753