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  2557  2euswapv  2623  2euswap  2638  disj  4413  ssunsn2  4791  prel12g  4828  disjiun  5095  soss  5566  wess  5624  frinxp  5721  trin2  6096  xp11  6148  oneqmini  6385  funss  6535  fvcofneq  7065  dff13  7229  f1cofveqaeq  7232  f1eqcocnv  7276  isores3  7310  isosolem  7322  isowe2  7325  trom  7851  f1oweALT  7951  f1o2ndf1  8101  suppofssd  8182  tposfn2  8227  tposf1o2  8231  frrlem4  8268  smo11  8333  tz7.48lem  8409  om00  8539  omsmo  8622  ixpfi2  9301  elfiun  9381  supmo  9403  infmo  9448  frmin  9702  cardaleph  10042  dfac5  10082  fin1a2lem9  10361  axdc3lem2  10404  zorn2lem6  10454  indpi  10860  genpnmax  10960  reclem3pr  11002  reclem4pr  11003  suplem1pr  11005  supsrlem  11064  dedekind  11337  lemul12b  12039  lbreu  12133  supadd  12151  supmullem2  12154  cju  12182  nnind  12204  uz11  12818  xrre2  13130  qbtwnre  13159  ico0  13352  ioc0  13353  ssfzoulel  13721  ishashinf  14428  swrdccatin2  14694  coss12d  14938  01sqrexlem6  15213  o1lo1  15503  ruclem9  16206  isprm3  16653  eulerthlem2  16752  prmdiveq  16756  ramub2  16985  cictr  17767  clatl  18467  lubun  18474  ipodrsima  18500  dirtr  18561  smndex1mgm  18834  smndex1sgrp  18835  smndex1mnd  18837  mulgpropd  19048  imasabl  19806  dprdss  19961  subrgdvds  20495  rhmsscrnghm  20574  dmatsubcl  22385  scmatcrng  22408  epttop  22896  cnprest  23176  lmmo  23267  lly1stc  23383  txcnp  23507  addcnlem  24753  clmvscom  24990  caussi  25197  bcthlem5  25228  ovollb2lem  25389  voliunlem1  25451  ioombl1lem4  25462  rolle  25894  c1lip1  25902  c1lip3  25904  ulmval  26289  sqf11  27049  fsumvma  27124  dchrelbas3  27149  nocvxminlem  27689  nocvxmin  27690  conway  27711  cofcut1  27828  precsexlem10  28118  acopy  28760  brbtwn2  28832  axeuclidlem  28889  axcontlem9  28899  axcontlem10  28900  umgrvad2edg  29140  upgrwlkdvdelem  29666  usgr2wlkneq  29686  2wlkdlem6  29861  umgr2adedgwlklem  29874  umgr2adedgspth  29878  2pthfrgrrn2  30212  frgrnbnb  30222  fusgr2wsp2nb  30263  nmcvcn  30624  sspmval  30662  sspimsval  30667  shsubcl  31149  shorth  31224  5oalem6  31588  strlem1  32179  atexch  32310  cdj3i  32370  xrofsup  32690  nnindf  32744  cnre2csqima  33901  nummin  35081  subgrwlk  35119  cusgr3cyclex  35123  erdszelem9  35186  erdsze2lem2  35191  gonarlem  35381  satffunlem  35388  satefvfmla1  35412  ss2mcls  35555  funpsstri  35753  dfon2lem4  35774  dfon2  35780  wsuclem  35813  elfuns  35903  btwnswapid  36005  ifscgr  36032  hilbert1.2  36143  elicc3  36305  tailfb  36365  bj-nnfand  36737  bj-gabss  36923  bj-imdirval3  37172  pibt2  37405  wl-mo3t  37564  ltflcei  37602  tan2h  37606  mblfinlem3  37653  fzmul  37735  metf1o  37749  ismtycnv  37796  ismtyres  37802  crngohomfo  38000  cossss  38416  funALTVss  38691  disjss  38723  hlhgt2  39383  hl2at  39399  2llnjN  39561  2lplnj  39614  linepsubN  39746  cdlemg33b0  40695  dvh3dim3N  41443  mapdh9a  41783  fltaccoprm  42628  iocinico  43201  clcnvlem  43612  ismnushort  44290  pm11.59  44380  f1cof1b  47078  afvres  47173  afv2res  47240  isuspgrim0lem  47893  isuspgrimlem  47895  ply1mulgsumlem1  48375  fldivexpfllog2  48554