Theorem anim12d 584

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anim12d1  585  anim1d  586  anim2d  587  prth  593  im2anan9  876  anim12dan  878  3anim123d  1398  mo3  2495  2euswap  2536  ssunsn2  4299  disjiun  4573  soss  4977  wess  5025  frinxp  5107  trin2  5438  xp11  5488  ordtri3OLD  5677  oneqmini  5693  funss  5822  fun  5979  fvcofneq  6275  dff13  6416  f1eqcocnv  6456  isores3  6485  isosolem  6497  isowe2  6500  ordom  6966  f1oweALT  7043  f1o2ndf1  7172  tposfn2  7261  tposf1o2  7265  wfrlem4  7305  smo11  7348  tz7.48lem  7423  om00  7542  omsmo  7621  ixpfi2  8147  elfiun  8219  supmo  8241  infmo  8284  alephord  8781  cardaleph  8795  dfac5  8834  fin1a2lem9  9113  axdc3lem2  9156  zorn2lem6  9206  grudomon  9518  indpi  9608  genpnmax  9708  reclem3pr  9750  reclem4pr  9751  suplem1pr  9753  supsrlem  9811  dedekind  10079  lemul12b  10759  fimaxre  10847  lbreu  10852  supadd  10868  supmullem2  10871  cju  10893  nnind  10915  uz11  11586  xrre2  11875  qbtwnre  11904  xrsupexmnf  12007  xrinfmexpnf  12008  ico0  12092  ioc0  12093  ssfzoulel  12428  ishashinf  13104  swrdccatin2  13338  coss12d  13559  sqrlem6  13836  o1lo1  14116  ruclem9  14806  isprm3  15234  eulerthlem2  15325  prmdiveq  15329  ramub2  15556  cictr  16288  joinfval  16824  meetfval  16838  clatl  16939  lubun  16946  ipodrsima  16988  dirtr  17059  mulgpropd  17407  dprdss  18251  subrgdvds  18617  dmatsubcl  20123  scmatcrng  20146  epttop  20623  cnpresti  20902  cnprest  20903  lmmo  20994  1stcrest  21066  lly1stc  21109  txcnp  21233  addcnlem  22475  clmvscom  22698  caussi  22903  bcthlem5  22933  ovollb2lem  23063  voliunlem1  23125  ioombl1lem4  23136  rolle  23557  c1lip1  23564  c1lip3  23566  ulmval  23938  sqf11  24665  fsumvma  24738  dchrelbas3  24763  acopy  25524  brbtwn2  25585  axeuclidlem  25642  axcontlem9  25652  axcontlem10  25653  usgra2adedgspthlem1  26139  usgra2adedgwlkon  26143  usgra2wlkspthlem2  26148  constr3trllem2  26179  4cycl4v4e  26194  4cycl4dv  26195  usg2wlkonot  26410  usg2wotspth  26411  eupai  26494  2pthfrgrarn2  26537  frgranbnb  26547  nmcvcn  26934  sspmval  26972  sspimsval  26977  sspph  27094  shsubcl  27461  shorth  27538  5oalem6  27902  strlem1  28493  atexch  28624  cdj3i  28684  xrofsup  28923  nnindf  28952  cnre2csqima  29285  erdszelem9  30435  erdsze2lem2  30440  ss2mcls  30719  funpsstri  30909  dfon2lem4  30935  dfon2  30941  trpredrec  30982  frmin  30983  wsuclem  31017  wsuclemOLD  31018  frrlem4  31027  nocvxminlem  31089  nocvxmin  31090  nofulllem5  31105  elfuns  31192  btwnswapid  31294  ifscgr  31321  hilbert1.2  31432  elicc3  31481  tailfb  31542  wl-mo3t  32537  ltflcei  32567  tan2h  32571  mblfinlem3  32618  fzmul  32707  metf1o  32721  ismtycnv  32771  ismtyres  32777  crngohomfo  32975  hlhgt2  33693  hl2at  33709  2llnjN  33871  2lplnj  33924  linepsubN  34056  cdlemg33b0  35007  dvh3dim3N  35756  mapdh9a  36097  iocinico  36816  clcnvlem  36949  pm11.59  37613  afvres  39901  f1cofveqaeq  40323  umgrvad2edg  40440  upgrwlkdvdelem  40942  usgr2wlkneq  40962  21wlkdlem6  41138  umgr2adedgwlklem  41151  umgr2adedgspth  41155  2pthfrgrrn2  41453  frgrnbnb  41463  frgr2wwlkeqm  41496  fusgr2wsp2nb  41498  rhmsscrnghm  41818  ply1mulgsumlem1  41968  fldivexpfllog2  42157