Theorem anim12d 583

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

Syntax hints:   → wi 4   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  anim12d1  584  anim1d  585  anim2d  586  prth  592  im2anan9  875  anim12dan  877  3anim123d  1397  mo3  2494  2euswap  2535  ssunsn2  4296  disjiun  4567  soss  4966  wess  5014  frinxp  5096  trin2  5424  xp11  5473  ordtri3OLD  5662  oneqmini  5678  funss  5807  fun  5964  fvcofneq  6259  dff13  6393  f1eqcocnv  6433  isores3  6462  isosolem  6474  isowe2  6477  ordom  6943  f1oweALT  7020  f1o2ndf1  7149  tposfn2  7238  tposf1o2  7242  wfrlem4  7282  smo11  7325  tz7.48lem  7400  om00  7519  omsmo  7598  ixpfi2  8124  elfiun  8196  supmo  8218  infmo  8261  alephord  8758  cardaleph  8772  dfac5  8811  fin1a2lem9  9090  axdc3lem2  9133  zorn2lem6  9183  grudomon  9495  indpi  9585  genpnmax  9685  reclem3pr  9727  reclem4pr  9728  suplem1pr  9730  supsrlem  9788  dedekind  10051  lemul12b  10731  fimaxre  10819  lbreu  10824  supadd  10840  supmullem2  10843  cju  10865  nnind  10887  uz11  11544  xrre2  11836  qbtwnre  11865  xrsupexmnf  11965  xrinfmexpnf  11966  ico0  12050  ioc0  12051  ssfzoulel  12385  ishashinf  13058  swrdccatin2  13286  coss12d  13507  sqrlem6  13784  o1lo1  14064  ruclem9  14754  isprm3  15182  eulerthlem2  15273  prmdiveq  15277  ramub2  15504  cictr  16236  joinfval  16772  meetfval  16786  clatl  16887  lubun  16894  ipodrsima  16936  dirtr  17007  mulgpropd  17355  dprdss  18199  subrgdvds  18565  dmatsubcl  20070  scmatcrng  20093  epttop  20570  cnpresti  20849  cnprest  20850  lmmo  20941  1stcrest  21013  lly1stc  21056  txcnp  21180  addcnlem  22422  clmvscom  22645  caussi  22847  bcthlem5  22877  ovollb2lem  23007  voliunlem1  23069  ioombl1lem4  23080  rolle  23501  c1lip1  23508  c1lip3  23510  ulmval  23882  sqf11  24609  fsumvma  24682  dchrelbas3  24707  acopy  25469  brbtwn2  25530  axeuclidlem  25587  axcontlem9  25597  axcontlem10  25598  usgra2adedgspthlem1  25932  usgra2adedgwlkon  25936  usgra2wlkspthlem2  25941  constr3trllem2  25972  4cycl4v4e  25987  4cycl4dv  25988  usg2wlkonot  26203  usg2wotspth  26204  eupai  26287  2pthfrgrarn2  26330  frgranbnb  26340  nmcvcn  26727  sspmval  26765  sspimsval  26770  sspph  26887  shsubcl  27254  shorth  27331  5oalem6  27695  strlem1  28286  atexch  28417  cdj3i  28477  xrofsup  28716  nnindf  28745  cnre2csqima  29078  erdszelem9  30228  erdsze2lem2  30233  ss2mcls  30512  funpsstri  30702  dfon2lem4  30728  dfon2  30734  trpredrec  30775  frmin  30776  wsuclem  30810  wsuclemOLD  30811  frrlem4  30820  nocvxminlem  30882  nocvxmin  30883  nofulllem5  30898  elfuns  30985  btwnswapid  31087  ifscgr  31114  hilbert1.2  31225  elicc3  31274  tailfb  31335  wl-mo3t  32320  ltflcei  32350  tan2h  32354  mblfinlem3  32401  fzmul  32490  metf1o  32504  ismtycnv  32554  ismtyres  32560  crngohomfo  32758  hlhgt2  33476  hl2at  33492  2llnjN  33654  2lplnj  33707  linepsubN  33839  cdlemg33b0  34790  dvh3dim3N  35539  mapdh9a  35880  iocinico  36599  clcnvlem  36732  pm11.59  37396  afvres  39685  f1cofveqaeq  40118  umgrvad2edg  40421  upgrwlkdvdelem  40923  usgr2wlkneq  40943  21wlkdlem6  41119  umgr2adedgwlklem  41132  umgr2adedgspth  41136  2pthfrgrrn2  41434  frgrnbnb  41444  frgr2wwlkeqm  41477  fusgr2wsp2nb  41479  rhmsscrnghm  41799  ply1mulgsumlem1  41949  fldivexpfllog2  42138