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  2591  2euswapv  2657  2euswap  2672  ssunsn2  4791  prel12g  4827  disjiun  5095  soss  5587  wess  5645  frinxp  5742  trin2  6121  xp11  6172  oneqmini  6415  funss  6556  fvcofneq  7089  dff13  7254  f1cofveqaeq  7257  f1eqcocnv  7305  isores3  7339  isosolem  7351  isowe2  7354  trom  7874  f1oweALT  7972  f1o2ndf1  8122  suppofssd  8204  tposfn2  8249  tposf1o2  8253  frrlem4  8291  smo11  8356  tz7.48lem  8433  om00  8565  omsmo  8649  ixpfi2  9320  elfiun  9403  supmo  9425  infmo  9470  frmin  9734  cardaleph  10095  dfac5  10134  fin1a2lem9  10413  axdc3lem2  10456  zorn2lem6  10506  indpi  10919  genpnmax  11019  reclem3pr  11061  reclem4pr  11062  suplem1pr  11064  supsrlem  11123  dedekind  11400  lemul12b  12099  lbreu  12192  supadd  12210  supmullem2  12213  cju  12241  nnind  12278  uz11  12915  xrre2  13224  qbtwnre  13253  ico0  13446  ioc0  13447  ssfzoulel  13818  ishashinf  14530  swrdccatin2  14800  coss12d  15047  01sqrexlem6  15336  o1lo1  15626  ruclem9  16330  isprm3  16777  eulerthlem2  16877  prmdiveq  16881  ramub2  17110  cictr  17898  clatl  18600  lubun  18607  ipodrsima  18633  dirtr  18694  smndex1mgm  19023  smndex1sgrp  19024  smndex1mnd  19026  mulgpropd  19243  imasabl  20007  dprdss  20162  crngrhmfo  20641  subrgdvds  20752  rhmsscrnghm  20831  dmatsubcl  22724  scmatcrng  22747  epttop  23238  cnprest  23518  lmmo  23609  lly1stc  23726  txcnp  23850  addcnlem  25095  clmvscom  25322  caussi  25529  bcthlem5  25560  ovollb2lem  25720  voliunlem1  25782  ioombl1lem4  25793  rolle  26222  c1lip1  26229  c1lip3  26231  ulmval  26616  sqf11  27376  fsumvma  27450  dchrelbas3  27475  nocvxminlem  28020  nocvxmin  28021  conway  28045  cofcut1  28186  precsexlem10  28482  acopy  29221  brbtwn2  29363  axeuclidlem  29420  axcontlem9  29430  axcontlem10  29431  umgrvad2edg  29674  subgrwlk  30149  upgrwlkdvdelem  30202  usgr2wlkneq  30222  2wlkdlem6  30400  umgr2adedgwlklem  30413  umgr2adedgspth  30417  2pthfrgrrn2  30764  frgrnbnb  30774  fusgr2wsp2nb  30815  nmcvcn  31177  sspmval  31215  sspimsval  31220  shsubcl  31702  shorth  31777  5oalem6  32141  strlem1  32732  atexch  32863  cdj3i  32923  xrofsup  33240  nnindf  33292  cnre2csqima  34423  nummin  35600  ackardcard  35695  cusgr3cyclex  35727  erdszelem9  35780  erdsze2lem2  35785  gonarlem  35975  satffunlem  35982  satefvfmla1  36006  ss2mcls  36149  funpsstri  36347  dfon2lem4  36365  dfon2  36371  wsuclem  36404  elfuns  36494  btwnswapid  36599  ifscgr  36626  hilbert1.2  36737  elicc3  36938  tailfb  36998  dfttc4lem2  37150  bj-nnfand  37490  bj-gabss  37681  bj-imdirval3  37938  pibt2  38173  wl-mo3t  38341  ltflcei  38364  tan2h  38368  mblfinlem3  38410  fzmul  38493  metf1o  38507  ismtycnv  38554  ismtyres  38560  crngohomfo  38758  cossss  39265  funALTVss  39534  disjss  39581  hlhgt2  40264  hl2at  40280  2llnjN  40442  2lplnj  40495  linepsubN  40627  cdlemg33b0  41576  dvh3dim3N  42324  mapdh9a  42664  fltaccoprm  43488  iocinico  44055  clcnvlem  44465  ismnushort  45127  pm11.59  45217  f1cof1b  47967  afvres  48062  afv2res  48129  isuspgrim0lem  48811  isuspgrimlem  48813  grlimprclnbgrvtx  48917  ply1mulgsumlem1  49318  fldivexpfllog2  49497