Theorem anim12d 610

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anim12d1  611  anim1d  612  anim2d  613  anim12dan  620  3anim123d  1444  mo3  2559  mo4  2561  2euswapv  2627  2euswap  2642  disj  4448  ssunsn2  4831  prel12g  4865  disjiun  5136  soss  5609  wess  5664  frinxp  5759  trin2  6125  xp11  6175  oneqmini  6417  funss  6568  fvcofneq  7095  dff13  7254  f1cofveqaeq  7257  f1eqcocnv  7299  f1eqcocnvOLD  7300  isores3  7332  isosolem  7344  isowe2  7347  trom  7864  f1oweALT  7959  f1o2ndf1  8108  suppofssd  8188  tposfn2  8233  tposf1o2  8237  frrlem4  8274  wfrlem4OLD  8312  smo11  8364  tz7.48lem  8441  om00  8575  omsmo  8657  ixpfi2  9350  elfiun  9425  supmo  9447  infmo  9490  frmin  9744  cardaleph  10084  dfac5  10123  fin1a2lem9  10403  axdc3lem2  10446  zorn2lem6  10496  indpi  10902  genpnmax  11002  reclem3pr  11044  reclem4pr  11045  suplem1pr  11047  supsrlem  11106  dedekind  11377  lemul12b  12071  lbreu  12164  supadd  12182  supmullem2  12185  cju  12208  nnind  12230  uz11  12847  xrre2  13149  qbtwnre  13178  ico0  13370  ioc0  13371  ssfzoulel  13726  ishashinf  14424  swrdccatin2  14679  coss12d  14919  01sqrexlem6  15194  o1lo1  15481  ruclem9  16181  isprm3  16620  eulerthlem2  16715  prmdiveq  16719  ramub2  16947  cictr  17752  clatl  18461  lubun  18468  ipodrsima  18494  dirtr  18555  smndex1mgm  18788  smndex1sgrp  18789  smndex1mnd  18791  mulgpropd  18996  imasabl  19744  dprdss  19899  subrgdvds  20333  dmatsubcl  22000  scmatcrng  22023  epttop  22512  cnprest  22793  lmmo  22884  lly1stc  23000  txcnp  23124  addcnlem  24380  clmvscom  24606  caussi  24814  bcthlem5  24845  ovollb2lem  25005  voliunlem1  25067  ioombl1lem4  25078  rolle  25507  c1lip1  25514  c1lip3  25516  ulmval  25892  sqf11  26643  fsumvma  26716  dchrelbas3  26741  nocvxminlem  27279  nocvxmin  27280  conway  27300  cofcut1  27407  precsexlem10  27662  acopy  28084  brbtwn2  28163  axeuclidlem  28220  axcontlem9  28230  axcontlem10  28231  umgrvad2edg  28470  upgrwlkdvdelem  28993  usgr2wlkneq  29013  2wlkdlem6  29185  umgr2adedgwlklem  29198  umgr2adedgspth  29202  2pthfrgrrn2  29536  frgrnbnb  29546  fusgr2wsp2nb  29587  nmcvcn  29948  sspmval  29986  sspimsval  29991  shsubcl  30473  shorth  30548  5oalem6  30912  strlem1  31503  atexch  31634  cdj3i  31694  xrofsup  31980  nnindf  32025  cnre2csqima  32891  nummin  34094  subgrwlk  34123  cusgr3cyclex  34127  erdszelem9  34190  erdsze2lem2  34195  gonarlem  34385  satffunlem  34392  satefvfmla1  34416  ss2mcls  34559  funpsstri  34737  dfon2lem4  34758  dfon2  34764  wsuclem  34797  elfuns  34887  btwnswapid  34989  ifscgr  35016  hilbert1.2  35127  elicc3  35202  tailfb  35262  bj-nnfand  35627  bj-gabss  35815  bj-imdirval3  36065  pibt2  36298  wl-mo3t  36441  ltflcei  36476  tan2h  36480  mblfinlem3  36527  fzmul  36609  metf1o  36623  ismtycnv  36670  ismtyres  36676  crngohomfo  36874  cossss  37295  funALTVss  37569  disjss  37601  hlhgt2  38260  hl2at  38276  2llnjN  38438  2lplnj  38491  linepsubN  38623  cdlemg33b0  39572  dvh3dim3N  40320  mapdh9a  40660  fltaccoprm  41382  iocinico  41961  clcnvlem  42374  ismnushort  43060  pm11.59  43150  f1cof1b  45785  afvres  45880  afv2res  45947  isomuspgrlem1  46495  isomuspgrlem2c  46498  isomuspgrlem2d  46499  rhmsscrnghm  46924  ply1mulgsumlem1  47067  fldivexpfllog2  47251