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  2558  2euswapv  2624  2euswap  2639  disj  4398  ssunsn2  4777  prel12g  4814  disjiun  5077  soss  5542  wess  5600  frinxp  5697  trin2  6067  xp11  6119  oneqmini  6355  funss  6496  fvcofneq  7021  dff13  7183  f1cofveqaeq  7186  f1eqcocnv  7230  isores3  7264  isosolem  7276  isowe2  7279  trom  7800  f1oweALT  7899  f1o2ndf1  8047  suppofssd  8128  tposfn2  8173  tposf1o2  8177  frrlem4  8214  smo11  8279  tz7.48lem  8355  om00  8485  omsmo  8568  ixpfi2  9229  elfiun  9309  supmo  9331  infmo  9376  frmin  9634  cardaleph  9972  dfac5  10012  fin1a2lem9  10291  axdc3lem2  10334  zorn2lem6  10384  indpi  10790  genpnmax  10890  reclem3pr  10932  reclem4pr  10933  suplem1pr  10935  supsrlem  10994  dedekind  11268  lemul12b  11970  lbreu  12064  supadd  12082  supmullem2  12085  cju  12113  nnind  12135  uz11  12749  xrre2  13061  qbtwnre  13090  ico0  13283  ioc0  13284  ssfzoulel  13652  ishashinf  14362  swrdccatin2  14628  coss12d  14871  01sqrexlem6  15146  o1lo1  15436  ruclem9  16139  isprm3  16586  eulerthlem2  16685  prmdiveq  16689  ramub2  16918  cictr  17704  clatl  18406  lubun  18413  ipodrsima  18439  dirtr  18500  smndex1mgm  18807  smndex1sgrp  18808  smndex1mnd  18810  mulgpropd  19021  imasabl  19781  dprdss  19936  subrgdvds  20494  rhmsscrnghm  20573  dmatsubcl  22406  scmatcrng  22429  epttop  22917  cnprest  23197  lmmo  23288  lly1stc  23404  txcnp  23528  addcnlem  24773  clmvscom  25010  caussi  25217  bcthlem5  25248  ovollb2lem  25409  voliunlem1  25471  ioombl1lem4  25482  rolle  25914  c1lip1  25922  c1lip3  25924  ulmval  26309  sqf11  27069  fsumvma  27144  dchrelbas3  27169  nocvxminlem  27710  nocvxmin  27711  conway  27733  cofcut1  27857  precsexlem10  28147  acopy  28804  brbtwn2  28876  axeuclidlem  28933  axcontlem9  28943  axcontlem10  28944  umgrvad2edg  29184  upgrwlkdvdelem  29707  usgr2wlkneq  29727  2wlkdlem6  29902  umgr2adedgwlklem  29915  umgr2adedgspth  29919  2pthfrgrrn2  30253  frgrnbnb  30263  fusgr2wsp2nb  30304  nmcvcn  30665  sspmval  30703  sspimsval  30708  shsubcl  31190  shorth  31265  5oalem6  31629  strlem1  32220  atexch  32351  cdj3i  32411  xrofsup  32740  nnindf  32792  cnre2csqima  33914  nummin  35093  subgrwlk  35144  cusgr3cyclex  35148  erdszelem9  35211  erdsze2lem2  35216  gonarlem  35406  satffunlem  35413  satefvfmla1  35437  ss2mcls  35580  funpsstri  35778  dfon2lem4  35799  dfon2  35805  wsuclem  35838  elfuns  35928  btwnswapid  36030  ifscgr  36057  hilbert1.2  36168  elicc3  36330  tailfb  36390  bj-nnfand  36762  bj-gabss  36948  bj-imdirval3  37197  pibt2  37430  wl-mo3t  37589  ltflcei  37627  tan2h  37631  mblfinlem3  37678  fzmul  37760  metf1o  37774  ismtycnv  37821  ismtyres  37827  crngohomfo  38025  cossss  38441  funALTVss  38716  disjss  38748  hlhgt2  39407  hl2at  39423  2llnjN  39585  2lplnj  39638  linepsubN  39770  cdlemg33b0  40719  dvh3dim3N  41467  mapdh9a  41807  fltaccoprm  42652  iocinico  43224  clcnvlem  43635  ismnushort  44313  pm11.59  44403  f1cof1b  47087  afvres  47182  afv2res  47249  isuspgrim0lem  47903  isuspgrimlem  47905  grlimprclnbgrvtx  48009  ply1mulgsumlem1  48397  fldivexpfllog2  48576