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 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  611  anim1d  612  anim2d  613  anim12dan  620  3anim123d  1446  mo3  2565  2euswapv  2631  2euswap  2646  ssunsn2  4784  prel12g  4821  disjiun  5087  soss  5553  wess  5611  frinxp  5708  trin2  6081  xp11  6134  oneqmini  6371  funss  6512  fvcofneq  7040  dff13  7202  f1cofveqaeq  7205  f1eqcocnv  7249  isores3  7283  isosolem  7295  isowe2  7298  trom  7819  f1oweALT  7918  f1o2ndf1  8066  suppofssd  8147  tposfn2  8192  tposf1o2  8196  frrlem4  8233  smo11  8298  tz7.48lem  8374  om00  8504  omsmo  8588  ixpfi2  9254  elfiun  9337  supmo  9359  infmo  9404  frmin  9665  cardaleph  10003  dfac5  10043  fin1a2lem9  10322  axdc3lem2  10365  zorn2lem6  10415  indpi  10822  genpnmax  10922  reclem3pr  10964  reclem4pr  10965  suplem1pr  10967  supsrlem  11026  dedekind  11300  lemul12b  12002  lbreu  12096  supadd  12114  supmullem2  12117  cju  12145  nnind  12167  uz11  12780  xrre2  13089  qbtwnre  13118  ico0  13311  ioc0  13312  ssfzoulel  13680  ishashinf  14390  swrdccatin2  14656  coss12d  14899  01sqrexlem6  15174  o1lo1  15464  ruclem9  16167  isprm3  16614  eulerthlem2  16713  prmdiveq  16717  ramub2  16946  cictr  17733  clatl  18435  lubun  18442  ipodrsima  18468  dirtr  18529  smndex1mgm  18836  smndex1sgrp  18837  smndex1mnd  18839  mulgpropd  19050  imasabl  19809  dprdss  19964  subrgdvds  20523  rhmsscrnghm  20602  dmatsubcl  22446  scmatcrng  22469  epttop  22957  cnprest  23237  lmmo  23328  lly1stc  23444  txcnp  23568  addcnlem  24813  clmvscom  25050  caussi  25257  bcthlem5  25288  ovollb2lem  25449  voliunlem1  25511  ioombl1lem4  25522  rolle  25954  c1lip1  25962  c1lip3  25964  ulmval  26349  sqf11  27109  fsumvma  27184  dchrelbas3  27209  nocvxminlem  27754  nocvxmin  27755  conway  27777  cofcut1  27902  precsexlem10  28197  acopy  28888  brbtwn2  28961  axeuclidlem  29018  axcontlem9  29028  axcontlem10  29029  umgrvad2edg  29269  upgrwlkdvdelem  29792  usgr2wlkneq  29812  2wlkdlem6  29987  umgr2adedgwlklem  30000  umgr2adedgspth  30004  2pthfrgrrn2  30341  frgrnbnb  30351  fusgr2wsp2nb  30392  nmcvcn  30753  sspmval  30791  sspimsval  30796  shsubcl  31278  shorth  31353  5oalem6  31717  strlem1  32308  atexch  32439  cdj3i  32499  xrofsup  32828  nnindf  32881  cnre2csqima  34049  nummin  35230  subgrwlk  35307  cusgr3cyclex  35311  erdszelem9  35374  erdsze2lem2  35379  gonarlem  35569  satffunlem  35576  satefvfmla1  35600  ss2mcls  35743  funpsstri  35941  dfon2lem4  35959  dfon2  35965  wsuclem  35998  elfuns  36088  btwnswapid  36192  ifscgr  36219  hilbert1.2  36330  elicc3  36492  tailfb  36552  bj-nnfand  36925  bj-gabss  37111  bj-imdirval3  37360  pibt2  37593  wl-mo3t  37752  ltflcei  37780  tan2h  37784  mblfinlem3  37831  fzmul  37913  metf1o  37927  ismtycnv  37974  ismtyres  37980  crngohomfo  38178  cossss  38687  funALTVss  38956  disjss  39003  hlhgt2  39686  hl2at  39702  2llnjN  39864  2lplnj  39917  linepsubN  40049  cdlemg33b0  40998  dvh3dim3N  41746  mapdh9a  42086  fltaccoprm  42919  iocinico  43490  clcnvlem  43900  ismnushort  44578  pm11.59  44668  f1cof1b  47359  afvres  47454  afv2res  47521  isuspgrim0lem  48175  isuspgrimlem  48177  grlimprclnbgrvtx  48281  ply1mulgsumlem1  48668  fldivexpfllog2  48847