Theorem anim12d 620

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anim12d1  621  anim1d  622  anim2d  623  anim12dan  630  3anim123d  1467  mo3  2594  2euswapv  2660  2euswap  2675  ssunsn2  4788  prel12g  4825  disjiun  5093  soss  5580  wess  5638  frinxp  5735  trin2  6114  xp11  6165  oneqmini  6403  funss  6544  fvcofneq  7078  dff13  7242  f1cofveqaeq  7245  f1eqcocnv  7289  isores3  7323  isosolem  7335  isowe2  7338  trom  7859  f1oweALT  7957  f1o2ndf1  8105  suppofssd  8187  tposfn2  8232  tposf1o2  8236  frrlem4  8274  smo11  8339  tz7.48lem  8416  om00  8548  omsmo  8632  ixpfi2  9295  elfiun  9378  supmo  9400  infmo  9445  frmin  9709  cardaleph  10061  dfac5  10100  fin1a2lem9  10380  axdc3lem2  10423  zorn2lem6  10473  indpi  10880  genpnmax  10980  reclem3pr  11022  reclem4pr  11023  suplem1pr  11025  supsrlem  11084  dedekind  11361  lemul12b  12063  lbreu  12156  supadd  12174  supmullem2  12177  cju  12205  nnind  12242  uz11  12878  xrre2  13187  qbtwnre  13216  ico0  13409  ioc0  13410  ssfzoulel  13780  ishashinf  14490  swrdccatin2  14756  coss12d  14999  01sqrexlem6  15288  o1lo1  15578  ruclem9  16284  isprm3  16731  eulerthlem2  16831  prmdiveq  16835  ramub2  17064  cictr  17852  clatl  18554  lubun  18561  ipodrsima  18587  dirtr  18648  smndex1mgm  18959  smndex1sgrp  18960  smndex1mnd  18962  mulgpropd  19173  imasabl  19937  dprdss  20092  subrgdvds  20662  rhmsscrnghm  20741  dmatsubcl  22616  scmatcrng  22639  epttop  23127  cnprest  23407  lmmo  23498  lly1stc  23614  txcnp  23738  addcnlem  24983  clmvscom  25210  caussi  25417  bcthlem5  25448  ovollb2lem  25608  voliunlem1  25670  ioombl1lem4  25681  rolle  26110  c1lip1  26117  c1lip3  26119  ulmval  26501  sqf11  27261  fsumvma  27335  dchrelbas3  27360  nocvxminlem  27905  nocvxmin  27906  conway  27930  cofcut1  28071  precsexlem10  28367  acopy  29085  brbtwn2  29164  axeuclidlem  29221  axcontlem9  29231  axcontlem10  29232  umgrvad2edg  29472  upgrwlkdvdelem  29994  usgr2wlkneq  30014  2wlkdlem6  30189  umgr2adedgwlklem  30202  umgr2adedgspth  30206  2pthfrgrrn2  30543  frgrnbnb  30553  fusgr2wsp2nb  30594  nmcvcn  30956  sspmval  30994  sspimsval  30999  shsubcl  31481  shorth  31556  5oalem6  31920  strlem1  32511  atexch  32642  cdj3i  32702  xrofsup  33024  nnindf  33077  cnre2csqima  34218  nummin  35399  subgrwlk  35495  cusgr3cyclex  35499  erdszelem9  35562  erdsze2lem2  35567  gonarlem  35757  satffunlem  35764  satefvfmla1  35788  ss2mcls  35931  funpsstri  36129  dfon2lem4  36147  dfon2  36153  wsuclem  36186  elfuns  36276  btwnswapid  36380  ifscgr  36407  hilbert1.2  36518  elicc3  36690  tailfb  36750  dfttc4lem2  36902  bj-nnfand  37242  bj-gabss  37432  bj-imdirval3  37688  pibt2  37923  wl-mo3t  38091  ltflcei  38119  tan2h  38123  mblfinlem3  38170  fzmul  38252  metf1o  38266  ismtycnv  38313  ismtyres  38319  crngohomfo  38517  cossss  39026  funALTVss  39295  disjss  39342  hlhgt2  40025  hl2at  40041  2llnjN  40203  2lplnj  40256  linepsubN  40388  cdlemg33b0  41337  dvh3dim3N  42085  mapdh9a  42425  fltaccoprm  43234  iocinico  43801  clcnvlem  44211  ismnushort  44875  pm11.59  44965  f1cof1b  47669  afvres  47764  afv2res  47831  isuspgrim0lem  48513  isuspgrimlem  48515  grlimprclnbgrvtx  48619  ply1mulgsumlem1  49017  fldivexpfllog2  49196