Theorem anim12d 620

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

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

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 401

This theorem is used by:  anim12d1  621  anim1d  622  anim2d  623  anim12dan  630  3anim123d  1470  mo3  2591  2euswapv  2657  2euswap  2672  ssunsn2  4792  prel12g  4828  disjiun  5096  soss  5588  wess  5646  frinxp  5743  trin2  6122  xp11  6172  oneqmini  6414  funss  6555  fvcofneq  7088  dff13  7252  f1cofveqaeq  7255  f1eqcocnv  7299  isores3  7333  isosolem  7345  isowe2  7348  trom  7869  f1oweALT  7967  f1o2ndf1  8115  suppofssd  8197  tposfn2  8242  tposf1o2  8246  frrlem4  8284  smo11  8349  tz7.48lem  8426  om00  8558  omsmo  8642  ixpfi2  9305  elfiun  9388  supmo  9410  infmo  9455  frmin  9719  cardaleph  10080  dfac5  10119  fin1a2lem9  10398  axdc3lem2  10441  zorn2lem6  10491  indpi  10898  genpnmax  10998  reclem3pr  11040  reclem4pr  11041  suplem1pr  11043  supsrlem  11102  dedekind  11379  lemul12b  12078  lbreu  12171  supadd  12189  supmullem2  12192  cju  12220  nnind  12257  uz11  12893  xrre2  13202  qbtwnre  13231  ico0  13424  ioc0  13425  ssfzoulel  13796  ishashinf  14507  swrdccatin2  14773  coss12d  15016  01sqrexlem6  15305  o1lo1  15595  ruclem9  16300  isprm3  16747  eulerthlem2  16847  prmdiveq  16851  ramub2  17080  cictr  17868  clatl  18570  lubun  18577  ipodrsima  18603  dirtr  18664  smndex1mgm  18975  smndex1sgrp  18976  smndex1mnd  18978  mulgpropd  19188  imasabl  19952  dprdss  20107  crngrhmfo  20585  subrgdvds  20696  rhmsscrnghm  20775  dmatsubcl  22666  scmatcrng  22689  epttop  23177  cnprest  23457  lmmo  23548  lly1stc  23664  txcnp  23788  addcnlem  25033  clmvscom  25260  caussi  25467  bcthlem5  25498  ovollb2lem  25658  voliunlem1  25720  ioombl1lem4  25731  rolle  26160  c1lip1  26167  c1lip3  26169  ulmval  26554  sqf11  27314  fsumvma  27388  dchrelbas3  27413  nocvxminlem  27958  nocvxmin  27959  conway  27983  cofcut1  28124  precsexlem10  28420  acopy  29155  brbtwn2  29266  axeuclidlem  29323  axcontlem9  29333  axcontlem10  29334  umgrvad2edg  29574  upgrwlkdvdelem  30096  usgr2wlkneq  30116  2wlkdlem6  30291  umgr2adedgwlklem  30304  umgr2adedgspth  30308  2pthfrgrrn2  30645  frgrnbnb  30655  fusgr2wsp2nb  30696  nmcvcn  31058  sspmval  31096  sspimsval  31101  shsubcl  31583  shorth  31658  5oalem6  32022  strlem1  32613  atexch  32744  cdj3i  32804  xrofsup  33123  nnindf  33175  cnre2csqima  34310  nummin  35493  ackardcard  35588  subgrwlk  35632  cusgr3cyclex  35636  erdszelem9  35699  erdsze2lem2  35704  gonarlem  35894  satffunlem  35901  satefvfmla1  35925  ss2mcls  36068  funpsstri  36266  dfon2lem4  36284  dfon2  36290  wsuclem  36323  elfuns  36413  btwnswapid  36517  ifscgr  36544  hilbert1.2  36655  elicc3  36856  tailfb  36916  dfttc4lem2  37068  bj-nnfand  37408  bj-gabss  37599  bj-imdirval3  37856  pibt2  38091  wl-mo3t  38259  ltflcei  38287  tan2h  38291  mblfinlem3  38338  fzmul  38420  metf1o  38434  ismtycnv  38481  ismtyres  38487  crngohomfo  38685  cossss  39192  funALTVss  39461  disjss  39508  hlhgt2  40191  hl2at  40207  2llnjN  40369  2lplnj  40422  linepsubN  40554  cdlemg33b0  41503  dvh3dim3N  42251  mapdh9a  42591  fltaccoprm  43400  iocinico  43967  clcnvlem  44377  ismnushort  45039  pm11.59  45129  f1cof1b  47842  afvres  47937  afv2res  48004  isuspgrim0lem  48686  isuspgrimlem  48688  grlimprclnbgrvtx  48792  ply1mulgsumlem1  49194  fldivexpfllog2  49373