Theorem anim12d 598

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  anim12d1  599  anim1d  600  anim2d  601  anim12dan  607  im2anan9  608  prth  834  3anim123d  1560  mo3  2670  2euswap  2712  ssunsn2  4548  prel12g  4586  disjiun  4832  soss  5250  wess  5298  frinxp  5386  trin2  5730  xp11  5780  oneqmini  5988  funss  6116  fun  6277  fvcofneq  6585  dff13  6732  f1cofveqaeq  6735  f1eqcocnv  6776  isores3  6805  isosolem  6817  isowe2  6820  ordom  7300  f1oweALT  7378  f1o2ndf1  7515  tposfn2  7605  tposf1o2  7609  wfrlem4  7649  wfrlem4OLD  7650  smo11  7693  tz7.48lem  7768  om00  7888  omsmo  7967  ixpfi2  8499  elfiun  8571  supmo  8593  infmo  8636  alephord  9177  cardaleph  9191  dfac5  9230  fin1a2lem9  9511  axdc3lem2  9554  zorn2lem6  9604  grudomon  9920  indpi  10010  genpnmax  10110  reclem3pr  10152  reclem4pr  10153  suplem1pr  10155  supsrlem  10213  dedekind  10481  lemul12b  11161  fimaxre  11249  lbreu  11254  supadd  11272  supmullem2  11275  cju  11297  nnind  11319  uz11  11923  xrre2  12215  qbtwnre  12244  xrsupexmnf  12349  xrinfmexpnf  12350  ico0  12435  ioc0  12436  ssfzoulel  12782  ishashinf  13460  swrdccatin2  13707  coss12d  13932  sqrlem6  14207  o1lo1  14487  ruclem9  15183  isprm3  15610  eulerthlem2  15700  prmdiveq  15704  ramub2  15931  cictr  16665  joinfval  17202  meetfval  17216  clatl  17317  lubun  17324  ipodrsima  17366  dirtr  17437  mulgpropd  17782  dprdss  18626  subrgdvds  18994  dmatsubcl  20511  scmatcrng  20534  epttop  21023  cnpresti  21302  cnprest  21303  lmmo  21394  1stcrest  21466  lly1stc  21509  txcnp  21633  addcnlem  22876  clmvscom  23098  caussi  23303  bcthlem5  23333  ovollb2lem  23465  voliunlem1  23527  ioombl1lem4  23538  rolle  23963  c1lip1  23970  c1lip3  23972  ulmval  24344  sqf11  25075  fsumvma  25148  dchrelbas3  25173  acopy  25934  brbtwn2  25995  axeuclidlem  26052  axcontlem9  26062  axcontlem10  26063  umgrvad2edg  26316  upgrwlkdvdelem  26856  usgr2wlkneq  26876  2wlkdlem6  27067  umgr2adedgwlklem  27080  umgr2adedgspth  27084  2pthfrgrrn2  27454  frgrnbnb  27464  fusgr2wsp2nb  27505  nmcvcn  27874  sspmval  27912  sspimsval  27917  sspph  28034  shsubcl  28401  shorth  28478  5oalem6  28842  strlem1  29433  atexch  29564  cdj3i  29624  xrofsup  29856  nnindf  29888  cnre2csqima  30278  erdszelem9  31499  erdsze2lem2  31504  ss2mcls  31783  funpsstri  31980  dfon2lem4  32006  dfon2  32012  trpredrec  32053  frmin  32058  wsuclem  32086  frrlem4  32099  nocvxminlem  32209  nocvxmin  32210  conway  32226  elfuns  32338  btwnswapid  32440  ifscgr  32467  hilbert1.2  32578  elicc3  32627  tailfb  32688  wl-mo3t  33667  ltflcei  33705  tan2h  33709  mblfinlem3  33756  fzmul  33843  metf1o  33857  ismtycnv  33907  ismtyres  33913  crngohomfo  34111  cossss  34488  hlhgt2  35164  hl2at  35180  2llnjN  35342  2lplnj  35395  linepsubN  35527  cdlemg33b0  36476  dvh3dim3N  37224  mapdh9a  37564  iocinico  38291  clcnvlem  38424  pm11.59  39085  afvres  41755  afv2res  41822  rhmsscrnghm  42588  ply1mulgsumlem1  42736  fldivexpfllog2  42921