Theorem anim12d 621

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anim12d1  622  anim1d  623  anim2d  624  anim12dan  631  3anim123d  1472  mo3  2592  2euswapv  2658  2euswap  2673  ssunsn2  4786  prel12g  4822  disjiun  5094  soss  5583  wess  5641  frinxp  5739  trin2  6129  xp11  6179  oneqmini  6434  funss  6578  fvcofneq  7117  dff13  7281  f1cofveqaeq  7284  f1eqcocnv  7332  isores3  7366  isosolem  7378  isowe2  7381  trom  7910  f1oweALT  8008  f1o2ndf1  8160  suppofssd  8248  tposfn2  8293  tposf1o2  8297  frrlem4  8335  smo11  8400  tz7.48lemOLD  8479  om00  8611  omsmo  8695  ixpfi2  9367  elfiun  9449  supmo  9471  infmo  9516  frmin  9780  cardaleph  10195  dfac5  10234  fin1a2lem9  10513  axdc3lem2  10556  zorn2lem6  10606  indpi  11019  genpnmax  11119  reclem3pr  11161  reclem4pr  11162  suplem1pr  11164  supsrlem  11223  dedekind  11500  lemul12b  12201  lbreu  12294  supadd  12312  supmullem2  12315  cju  12343  nnind  12380  uz11  13017  xrre2  13327  qbtwnre  13356  ico0  13549  ioc0  13550  ssfzoulel  13922  ishashinf  14635  swrdccatin2  14906  coss12d  15154  01sqrexlem6  15443  o1lo1  15733  ruclem9  16435  isprm3  16887  eulerthlem2  16988  prmdiveq  16992  ramub2  17221  cictr  18009  clatl  18711  lubun  18718  ipodrsima  18744  dirtr  18805  smndex1mgm  19135  smndex1sgrp  19136  smndex1mnd  19138  mulgpropd  19355  imasabl  20120  dprdss  20275  crngrhmfo  20756  subrgdvds  20868  rhmsscrnghm  20947  dmatsubcl  22843  scmatcrng  22866  epttop  23357  cnprest  23637  lmmo  23728  lly1stc  23845  txcnp  23969  addcnlem  25214  clmvscom  25441  caussi  25648  bcthlem5  25679  ovollb2lem  25839  voliunlem1  25901  ioombl1lem4  25912  rolle  26340  c1lip1  26347  c1lip3  26349  ulmval  26737  sqf11  27496  fsumvma  27570  dchrelbas3  27595  fltaccoprm  28002  nocvxminlem  28170  nocvxmin  28171  conway  28195  cofcut1  28336  precsexlem10  28632  acopy  29371  brbtwn2  29513  axeuclidlem  29570  axcontlem9  29580  axcontlem10  29581  umgrvad2edg  29824  subgrwlk  30299  upgrwlkdvdelem  30352  usgr2wlkneq  30372  2wlkdlem6  30550  umgr2adedgwlklem  30563  umgr2adedgspth  30567  2pthfrgrrn2  30914  frgrnbnb  30924  fusgr2wsp2nb  30965  nmcvcn  31327  sspmval  31365  sspimsval  31370  shsubcl  31852  shorth  31927  5oalem6  32291  strlem1  32882  atexch  33013  cdj3i  33073  xrofsup  33429  nnindf  33481  cnre2csqima  34613  mpofvop2d  35799  nummin  35806  ackardcard  35935  cusgr3cyclex  36068  erdszelem9  36131  erdsze2lem2  36136  gonarlem  36326  satffunlem  36333  satefvfmla1  36357  ss2mcls  36500  funpsstri  36709  dfon2lem4  36726  dfon2  36732  wsuclem  36765  elfuns  36855  btwnswapid  36960  ifscgr  36987  hilbert1.2  37098  elicc3  37283  tailfb  37343  dfttc4lem2  37495  bj-nnfand  37835  bj-gabss  38026  bj-imdirval3  38297  pibt2  38532  wl-mo3t  38700  ltflcei  38723  tan2h  38727  mblfinlem3  38769  fzmul  38867  metf1o  38881  ismtycnv  38928  ismtyres  38934  crngohomfo  39132  cossss  39639  funALTVss  39908  disjss  39955  hlhgt2  40638  hl2at  40654  2llnjN  40816  2lplnj  40869  linepsubN  41001  cdlemg33b0  41950  dvh3dim3N  42698  mapdh9a  43038  iocinico  44406  clcnvlem  44815  ismnushort  45477  pm11.59  45567  f1cof1b  48352  afvres  48447  afv2res  48514  isuspgrim0lem  49196  isuspgrimlem  49198  grlimprclnbgrvtx  49302  ply1mulgsumlem1  49703  fldivexpfllog2  49882