Theorem anim12d 609

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  anim12d1  610  anim1d  611  anim2d  612  anim12dan  619  3anim123d  1443  mo3  2558  mo4  2560  2euswapv  2626  2euswap  2641  disj  4447  ssunsn2  4830  prel12g  4864  disjiun  5135  soss  5608  wess  5663  frinxp  5758  trin2  6124  xp11  6174  oneqmini  6416  funss  6567  fvcofneq  7094  dff13  7256  f1cofveqaeq  7259  f1eqcocnv  7301  f1eqcocnvOLD  7302  isores3  7334  isosolem  7346  isowe2  7349  trom  7866  f1oweALT  7961  f1o2ndf1  8110  suppofssd  8190  tposfn2  8235  tposf1o2  8239  frrlem4  8276  wfrlem4OLD  8314  smo11  8366  tz7.48lem  8443  om00  8577  omsmo  8659  ixpfi2  9352  elfiun  9427  supmo  9449  infmo  9492  frmin  9746  cardaleph  10086  dfac5  10125  fin1a2lem9  10405  axdc3lem2  10448  zorn2lem6  10498  indpi  10904  genpnmax  11004  reclem3pr  11046  reclem4pr  11047  suplem1pr  11049  supsrlem  11108  dedekind  11381  lemul12b  12075  lbreu  12168  supadd  12186  supmullem2  12189  cju  12212  nnind  12234  uz11  12851  xrre2  13153  qbtwnre  13182  ico0  13374  ioc0  13375  ssfzoulel  13730  ishashinf  14428  swrdccatin2  14683  coss12d  14923  01sqrexlem6  15198  o1lo1  15485  ruclem9  16185  isprm3  16624  eulerthlem2  16719  prmdiveq  16723  ramub2  16951  cictr  17756  clatl  18465  lubun  18472  ipodrsima  18498  dirtr  18559  smndex1mgm  18824  smndex1sgrp  18825  smndex1mnd  18827  mulgpropd  19032  imasabl  19785  dprdss  19940  subrgdvds  20476  dmatsubcl  22220  scmatcrng  22243  epttop  22732  cnprest  23013  lmmo  23104  lly1stc  23220  txcnp  23344  addcnlem  24600  clmvscom  24830  caussi  25038  bcthlem5  25069  ovollb2lem  25229  voliunlem1  25291  ioombl1lem4  25302  rolle  25731  c1lip1  25738  c1lip3  25740  ulmval  26116  sqf11  26867  fsumvma  26940  dchrelbas3  26965  nocvxminlem  27503  nocvxmin  27504  conway  27525  cofcut1  27633  precsexlem10  27889  acopy  28339  brbtwn2  28418  axeuclidlem  28475  axcontlem9  28485  axcontlem10  28486  umgrvad2edg  28725  upgrwlkdvdelem  29248  usgr2wlkneq  29268  2wlkdlem6  29440  umgr2adedgwlklem  29453  umgr2adedgspth  29457  2pthfrgrrn2  29791  frgrnbnb  29801  fusgr2wsp2nb  29842  nmcvcn  30203  sspmval  30241  sspimsval  30246  shsubcl  30728  shorth  30803  5oalem6  31167  strlem1  31758  atexch  31889  cdj3i  31949  xrofsup  32235  nnindf  32280  cnre2csqima  33177  nummin  34380  subgrwlk  34409  cusgr3cyclex  34413  erdszelem9  34476  erdsze2lem2  34481  gonarlem  34671  satffunlem  34678  satefvfmla1  34702  ss2mcls  34845  funpsstri  35029  dfon2lem4  35050  dfon2  35056  wsuclem  35089  elfuns  35179  btwnswapid  35281  ifscgr  35308  hilbert1.2  35419  elicc3  35505  tailfb  35565  bj-nnfand  35930  bj-gabss  36118  bj-imdirval3  36368  pibt2  36601  wl-mo3t  36744  ltflcei  36779  tan2h  36783  mblfinlem3  36830  fzmul  36912  metf1o  36926  ismtycnv  36973  ismtyres  36979  crngohomfo  37177  cossss  37598  funALTVss  37872  disjss  37904  hlhgt2  38563  hl2at  38579  2llnjN  38741  2lplnj  38794  linepsubN  38926  cdlemg33b0  39875  dvh3dim3N  40623  mapdh9a  40963  fltaccoprm  41684  iocinico  42263  clcnvlem  42676  ismnushort  43362  pm11.59  43452  f1cof1b  46084  afvres  46179  afv2res  46246  isomuspgrlem1  46794  isomuspgrlem2c  46797  isomuspgrlem2d  46798  rhmsscrnghm  47013  ply1mulgsumlem1  47155  fldivexpfllog2  47339