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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anim12d1  621  anim1d  622  anim2d  623  anim12dan  630  3anim123d  1469  mo3  2590  2euswapv  2656  2euswap  2671  ssunsn2  4792  prel12g  4828  disjiun  5096  soss  5589  wess  5647  frinxp  5744  trin2  6123  xp11  6173  oneqmini  6414  funss  6555  fvcofneq  7088  dff13  7252  f1cofveqaeq  7255  f1eqcocnv  7299  isores3  7333  isosolem  7345  isowe2  7348  trom  7870  f1oweALT  7968  f1o2ndf1  8116  suppofssd  8198  tposfn2  8243  tposf1o2  8247  frrlem4  8285  smo11  8350  tz7.48lem  8427  om00  8559  omsmo  8643  ixpfi2  9306  elfiun  9389  supmo  9411  infmo  9456  frmin  9720  cardaleph  10072  dfac5  10111  fin1a2lem9  10391  axdc3lem2  10434  zorn2lem6  10484  indpi  10891  genpnmax  10991  reclem3pr  11033  reclem4pr  11034  suplem1pr  11036  supsrlem  11095  dedekind  11372  lemul12b  12071  lbreu  12164  supadd  12182  supmullem2  12185  cju  12213  nnind  12250  uz11  12886  xrre2  13195  qbtwnre  13224  ico0  13417  ioc0  13418  ssfzoulel  13789  ishashinf  14500  swrdccatin2  14766  coss12d  15009  01sqrexlem6  15298  o1lo1  15588  ruclem9  16293  isprm3  16740  eulerthlem2  16840  prmdiveq  16844  ramub2  17073  cictr  17861  clatl  18563  lubun  18570  ipodrsima  18596  dirtr  18657  smndex1mgm  18968  smndex1sgrp  18969  smndex1mnd  18971  mulgpropd  19181  imasabl  19945  dprdss  20100  subrgdvds  20670  rhmsscrnghm  20749  dmatsubcl  22634  scmatcrng  22657  epttop  23145  cnprest  23425  lmmo  23516  lly1stc  23632  txcnp  23756  addcnlem  25001  clmvscom  25228  caussi  25435  bcthlem5  25466  ovollb2lem  25626  voliunlem1  25688  ioombl1lem4  25699  rolle  26128  c1lip1  26135  c1lip3  26137  ulmval  26519  sqf11  27279  fsumvma  27353  dchrelbas3  27378  nocvxminlem  27923  nocvxmin  27924  conway  27948  cofcut1  28089  precsexlem10  28385  acopy  29117  brbtwn2  29221  axeuclidlem  29278  axcontlem9  29288  axcontlem10  29289  umgrvad2edg  29529  upgrwlkdvdelem  30051  usgr2wlkneq  30071  2wlkdlem6  30246  umgr2adedgwlklem  30259  umgr2adedgspth  30263  2pthfrgrrn2  30600  frgrnbnb  30610  fusgr2wsp2nb  30651  nmcvcn  31013  sspmval  31051  sspimsval  31056  shsubcl  31538  shorth  31613  5oalem6  31977  strlem1  32568  atexch  32699  cdj3i  32759  xrofsup  33078  nnindf  33130  cnre2csqima  34267  nummin  35450  ackardcard  35546  subgrwlk  35590  cusgr3cyclex  35594  erdszelem9  35657  erdsze2lem2  35662  gonarlem  35852  satffunlem  35859  satefvfmla1  35883  ss2mcls  36026  funpsstri  36224  dfon2lem4  36242  dfon2  36248  wsuclem  36281  elfuns  36371  btwnswapid  36475  ifscgr  36502  hilbert1.2  36613  elicc3  36794  tailfb  36854  dfttc4lem2  37006  bj-nnfand  37346  bj-gabss  37537  bj-imdirval3  37794  pibt2  38029  wl-mo3t  38197  ltflcei  38225  tan2h  38229  mblfinlem3  38276  fzmul  38358  metf1o  38372  ismtycnv  38419  ismtyres  38425  crngohomfo  38623  cossss  39132  funALTVss  39401  disjss  39448  hlhgt2  40131  hl2at  40147  2llnjN  40309  2lplnj  40362  linepsubN  40494  cdlemg33b0  41443  dvh3dim3N  42191  mapdh9a  42531  fltaccoprm  43342  iocinico  43909  clcnvlem  44319  ismnushort  44981  pm11.59  45071  f1cof1b  47781  afvres  47876  afv2res  47943  isuspgrim0lem  48625  isuspgrimlem  48627  grlimprclnbgrvtx  48731  ply1mulgsumlem1  49133  fldivexpfllog2  49312