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 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 207  df-an 396

This theorem is referenced by:  anim12d1  610  anim1d  611  anim2d  612  anim12dan  619  3anim123d  1445  mo3  2561  2euswapv  2627  2euswap  2642  ssunsn2  4780  prel12g  4817  disjiun  5083  soss  5549  wess  5607  frinxp  5704  trin2  6077  xp11  6130  oneqmini  6367  funss  6508  fvcofneq  7035  dff13  7197  f1cofveqaeq  7200  f1eqcocnv  7244  isores3  7278  isosolem  7290  isowe2  7293  trom  7814  f1oweALT  7913  f1o2ndf1  8061  suppofssd  8142  tposfn2  8187  tposf1o2  8191  frrlem4  8228  smo11  8293  tz7.48lem  8369  om00  8499  omsmo  8582  ixpfi2  9244  elfiun  9324  supmo  9346  infmo  9391  frmin  9652  cardaleph  9990  dfac5  10030  fin1a2lem9  10309  axdc3lem2  10352  zorn2lem6  10402  indpi  10808  genpnmax  10908  reclem3pr  10950  reclem4pr  10951  suplem1pr  10953  supsrlem  11012  dedekind  11286  lemul12b  11988  lbreu  12082  supadd  12100  supmullem2  12103  cju  12131  nnind  12153  uz11  12767  xrre2  13079  qbtwnre  13108  ico0  13301  ioc0  13302  ssfzoulel  13670  ishashinf  14380  swrdccatin2  14646  coss12d  14889  01sqrexlem6  15164  o1lo1  15454  ruclem9  16157  isprm3  16604  eulerthlem2  16703  prmdiveq  16707  ramub2  16936  cictr  17722  clatl  18424  lubun  18431  ipodrsima  18457  dirtr  18518  smndex1mgm  18825  smndex1sgrp  18826  smndex1mnd  18828  mulgpropd  19039  imasabl  19798  dprdss  19953  subrgdvds  20511  rhmsscrnghm  20590  dmatsubcl  22423  scmatcrng  22446  epttop  22934  cnprest  23214  lmmo  23305  lly1stc  23421  txcnp  23545  addcnlem  24790  clmvscom  25027  caussi  25234  bcthlem5  25265  ovollb2lem  25426  voliunlem1  25488  ioombl1lem4  25499  rolle  25931  c1lip1  25939  c1lip3  25941  ulmval  26326  sqf11  27086  fsumvma  27161  dchrelbas3  27186  nocvxminlem  27727  nocvxmin  27728  conway  27750  cofcut1  27874  precsexlem10  28164  acopy  28821  brbtwn2  28894  axeuclidlem  28951  axcontlem9  28961  axcontlem10  28962  umgrvad2edg  29202  upgrwlkdvdelem  29725  usgr2wlkneq  29745  2wlkdlem6  29920  umgr2adedgwlklem  29933  umgr2adedgspth  29937  2pthfrgrrn2  30274  frgrnbnb  30284  fusgr2wsp2nb  30325  nmcvcn  30686  sspmval  30724  sspimsval  30729  shsubcl  31211  shorth  31286  5oalem6  31650  strlem1  32241  atexch  32372  cdj3i  32432  xrofsup  32761  nnindf  32813  cnre2csqima  33935  nummin  35115  subgrwlk  35187  cusgr3cyclex  35191  erdszelem9  35254  erdsze2lem2  35259  gonarlem  35449  satffunlem  35456  satefvfmla1  35480  ss2mcls  35623  funpsstri  35821  dfon2lem4  35839  dfon2  35845  wsuclem  35878  elfuns  35968  btwnswapid  36072  ifscgr  36099  hilbert1.2  36210  elicc3  36372  tailfb  36432  bj-nnfand  36804  bj-gabss  36990  bj-imdirval3  37239  pibt2  37472  wl-mo3t  37631  ltflcei  37658  tan2h  37662  mblfinlem3  37709  fzmul  37791  metf1o  37805  ismtycnv  37852  ismtyres  37858  crngohomfo  38056  cossss  38537  funALTVss  38807  disjss  38839  hlhgt2  39498  hl2at  39514  2llnjN  39676  2lplnj  39729  linepsubN  39861  cdlemg33b0  40810  dvh3dim3N  41558  mapdh9a  41898  fltaccoprm  42748  iocinico  43319  clcnvlem  43730  ismnushort  44408  pm11.59  44498  f1cof1b  47191  afvres  47286  afv2res  47353  isuspgrim0lem  48007  isuspgrimlem  48009  grlimprclnbgrvtx  48113  ply1mulgsumlem1  48501  fldivexpfllog2  48680