Theorem anim12d 615

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anim12d1  616  anim1d  617  anim2d  618  anim12dan  625  3anim123d  1451  mo3  2568  2euswapv  2634  2euswap  2649  ssunsn2  4765  prel12g  4802  disjiun  5067  soss  5553  wess  5611  frinxp  5708  trin2  6080  xp11  6133  oneqmini  6370  funss  6511  fvcofneq  7041  dff13  7205  f1cofveqaeq  7208  f1eqcocnv  7252  isores3  7286  isosolem  7298  isowe2  7301  trom  7822  f1oweALT  7921  f1o2ndf1  8068  suppofssd  8150  tposfn2  8195  tposf1o2  8199  frrlem4  8236  smo11  8301  tz7.48lem  8377  om00  8507  omsmo  8591  ixpfi2  9257  elfiun  9340  supmo  9362  infmo  9407  frmin  9671  cardaleph  10009  dfac5  10049  fin1a2lem9  10328  axdc3lem2  10371  zorn2lem6  10421  indpi  10828  genpnmax  10928  reclem3pr  10970  reclem4pr  10971  suplem1pr  10973  supsrlem  11032  dedekind  11307  lemul12b  12010  lbreu  12104  supadd  12122  supmullem2  12125  cju  12153  nnind  12190  uz11  12811  xrre2  13120  qbtwnre  13149  ico0  13342  ioc0  13343  ssfzoulel  13713  ishashinf  14423  swrdccatin2  14689  coss12d  14932  01sqrexlem6  15207  o1lo1  15497  ruclem9  16203  isprm3  16650  eulerthlem2  16750  prmdiveq  16754  ramub2  16983  cictr  17770  clatl  18472  lubun  18479  ipodrsima  18505  dirtr  18566  smndex1mgm  18876  smndex1sgrp  18877  smndex1mnd  18879  mulgpropd  19090  imasabl  19849  dprdss  20004  subrgdvds  20565  rhmsscrnghm  20644  dmatsubcl  22488  scmatcrng  22511  epttop  22999  cnprest  23279  lmmo  23370  lly1stc  23486  txcnp  23610  addcnlem  24855  clmvscom  25082  caussi  25289  bcthlem5  25320  ovollb2lem  25480  voliunlem1  25542  ioombl1lem4  25553  rolle  25982  c1lip1  25989  c1lip3  25991  ulmval  26370  sqf11  27127  fsumvma  27201  dchrelbas3  27226  nocvxminlem  27771  nocvxmin  27772  conway  27796  cofcut1  27937  precsexlem10  28233  acopy  28926  brbtwn2  28999  axeuclidlem  29056  axcontlem9  29066  axcontlem10  29067  umgrvad2edg  29307  upgrwlkdvdelem  29829  usgr2wlkneq  29849  2wlkdlem6  30024  umgr2adedgwlklem  30037  umgr2adedgspth  30041  2pthfrgrrn2  30378  frgrnbnb  30388  fusgr2wsp2nb  30429  nmcvcn  30791  sspmval  30829  sspimsval  30834  shsubcl  31316  shorth  31391  5oalem6  31755  strlem1  32346  atexch  32477  cdj3i  32537  xrofsup  32866  nnindf  32919  cnre2csqima  34102  nummin  35283  subgrwlk  35361  cusgr3cyclex  35365  erdszelem9  35428  erdsze2lem2  35433  gonarlem  35623  satffunlem  35630  satefvfmla1  35654  ss2mcls  35797  funpsstri  35995  dfon2lem4  36013  dfon2  36019  wsuclem  36052  elfuns  36142  btwnswapid  36246  ifscgr  36273  hilbert1.2  36384  elicc3  36546  tailfb  36606  dfttc4lem2  36758  bj-nnfand  37099  bj-gabss  37289  bj-imdirval3  37545  pibt2  37780  wl-mo3t  37948  ltflcei  37976  tan2h  37980  mblfinlem3  38027  fzmul  38109  metf1o  38123  ismtycnv  38170  ismtyres  38176  crngohomfo  38374  cossss  38883  funALTVss  39152  disjss  39199  hlhgt2  39882  hl2at  39898  2llnjN  40060  2lplnj  40113  linepsubN  40245  cdlemg33b0  41194  dvh3dim3N  41942  mapdh9a  42282  fltaccoprm  43091  iocinico  43658  clcnvlem  44068  ismnushort  44746  pm11.59  44836  f1cof1b  47541  afvres  47636  afv2res  47703  isuspgrim0lem  48385  isuspgrimlem  48387  grlimprclnbgrvtx  48491  ply1mulgsumlem1  48878  fldivexpfllog2  49057