Theorem anim12d 608

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

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  anim12d1  609  anim1d  610  anim2d  611  anim12dan  618  3anim123d  1441  mo3  2564  mo4  2566  2euswapv  2632  2euswap  2647  disj  4378  ssunsn2  4757  prel12g  4791  disjiun  5057  soss  5514  wess  5567  frinxp  5660  trin2  6017  xp11  6067  oneqmini  6302  funss  6437  fvcofneq  6951  dff13  7109  f1cofveqaeq  7112  f1eqcocnv  7153  f1eqcocnvOLD  7154  isores3  7186  isosolem  7198  isowe2  7201  trom  7696  f1oweALT  7788  f1o2ndf1  7934  suppofssd  7990  tposfn2  8035  tposf1o2  8039  frrlem4  8076  wfrlem4OLD  8114  smo11  8166  tz7.48lem  8242  om00  8368  omsmo  8448  ixpfi2  9047  elfiun  9119  supmo  9141  infmo  9184  trpredrec  9415  frmin  9438  cardaleph  9776  dfac5  9815  fin1a2lem9  10095  axdc3lem2  10138  zorn2lem6  10188  indpi  10594  genpnmax  10694  reclem3pr  10736  reclem4pr  10737  suplem1pr  10739  supsrlem  10798  dedekind  11068  lemul12b  11762  lbreu  11855  supadd  11873  supmullem2  11876  cju  11899  nnind  11921  uz11  12536  xrre2  12833  qbtwnre  12862  ico0  13054  ioc0  13055  ssfzoulel  13409  ishashinf  14105  swrdccatin2  14370  coss12d  14611  sqrlem6  14887  o1lo1  15174  ruclem9  15875  isprm3  16316  eulerthlem2  16411  prmdiveq  16415  ramub2  16643  cictr  17434  clatl  18141  lubun  18148  ipodrsima  18174  dirtr  18235  smndex1mgm  18461  smndex1sgrp  18462  smndex1mnd  18464  mulgpropd  18660  dprdss  19547  subrgdvds  19953  dmatsubcl  21555  scmatcrng  21578  epttop  22067  cnprest  22348  lmmo  22439  lly1stc  22555  txcnp  22679  addcnlem  23933  clmvscom  24159  caussi  24366  bcthlem5  24397  ovollb2lem  24557  voliunlem1  24619  ioombl1lem4  24630  rolle  25059  c1lip1  25066  c1lip3  25068  ulmval  25444  sqf11  26193  fsumvma  26266  dchrelbas3  26291  acopy  27098  brbtwn2  27176  axeuclidlem  27233  axcontlem9  27243  axcontlem10  27244  umgrvad2edg  27483  upgrwlkdvdelem  28005  usgr2wlkneq  28025  2wlkdlem6  28197  umgr2adedgwlklem  28210  umgr2adedgspth  28214  2pthfrgrrn2  28548  frgrnbnb  28558  fusgr2wsp2nb  28599  nmcvcn  28958  sspmval  28996  sspimsval  29001  shsubcl  29483  shorth  29558  5oalem6  29922  strlem1  30513  atexch  30644  cdj3i  30704  xrofsup  30992  nnindf  31035  cnre2csqima  31763  nummin  32963  subgrwlk  32994  cusgr3cyclex  32998  erdszelem9  33061  erdsze2lem2  33066  gonarlem  33256  satffunlem  33263  satefvfmla1  33287  ss2mcls  33430  funpsstri  33645  dfon2lem4  33668  dfon2  33674  wsuclem  33746  nocvxminlem  33899  nocvxmin  33900  conway  33920  cofcut1  34017  elfuns  34144  btwnswapid  34246  ifscgr  34273  hilbert1.2  34384  elicc3  34433  tailfb  34493  bj-nnfand  34858  bj-gabss  35050  bj-imdirval3  35282  pibt2  35515  wl-mo3t  35658  ltflcei  35692  tan2h  35696  mblfinlem3  35743  fzmul  35826  metf1o  35840  ismtycnv  35887  ismtyres  35893  crngohomfo  36091  cossss  36475  funALTVss  36737  disjss  36769  hlhgt2  37330  hl2at  37346  2llnjN  37508  2lplnj  37561  linepsubN  37693  cdlemg33b0  38642  dvh3dim3N  39390  mapdh9a  39730  fltaccoprm  40393  iocinico  40959  clcnvlem  41120  ismnushort  41808  pm11.59  41898  f1cof1b  44456  afvres  44551  afv2res  44618  isomuspgrlem1  45167  isomuspgrlem2c  45170  isomuspgrlem2d  45171  rhmsscrnghm  45472  ply1mulgsumlem1  45615  fldivexpfllog2  45799