Theorem anim12d 610

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 609	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  611  anim1d  612  anim2d  613  anim12dan  620  3anim123d  1446  mo3  2565  2euswapv  2631  2euswap  2646  ssunsn2  4771  prel12g  4808  disjiun  5074  soss  5550  wess  5608  frinxp  5705  trin2  6078  xp11  6131  oneqmini  6368  funss  6509  fvcofneq  7037  dff13  7200  f1cofveqaeq  7203  f1eqcocnv  7247  isores3  7281  isosolem  7293  isowe2  7296  trom  7817  f1oweALT  7916  f1o2ndf1  8063  suppofssd  8144  tposfn2  8189  tposf1o2  8193  frrlem4  8230  smo11  8295  tz7.48lem  8371  om00  8501  omsmo  8585  ixpfi2  9251  elfiun  9334  supmo  9356  infmo  9401  frmin  9662  cardaleph  10000  dfac5  10040  fin1a2lem9  10319  axdc3lem2  10362  zorn2lem6  10412  indpi  10819  genpnmax  10919  reclem3pr  10961  reclem4pr  10962  suplem1pr  10964  supsrlem  11023  dedekind  11298  lemul12b  12001  lbreu  12095  supadd  12113  supmullem2  12116  cju  12144  nnind  12181  uz11  12802  xrre2  13111  qbtwnre  13140  ico0  13333  ioc0  13334  ssfzoulel  13704  ishashinf  14414  swrdccatin2  14680  coss12d  14923  01sqrexlem6  15198  o1lo1  15488  ruclem9  16194  isprm3  16641  eulerthlem2  16741  prmdiveq  16745  ramub2  16974  cictr  17761  clatl  18463  lubun  18470  ipodrsima  18496  dirtr  18557  smndex1mgm  18867  smndex1sgrp  18868  smndex1mnd  18870  mulgpropd  19081  imasabl  19840  dprdss  19995  subrgdvds  20552  rhmsscrnghm  20631  dmatsubcl  22472  scmatcrng  22495  epttop  22983  cnprest  23263  lmmo  23354  lly1stc  23470  txcnp  23594  addcnlem  24839  clmvscom  25066  caussi  25273  bcthlem5  25304  ovollb2lem  25464  voliunlem1  25526  ioombl1lem4  25537  rolle  25966  c1lip1  25974  c1lip3  25976  ulmval  26360  sqf11  27120  fsumvma  27195  dchrelbas3  27220  nocvxminlem  27765  nocvxmin  27766  conway  27790  cofcut1  27931  precsexlem10  28227  acopy  28920  brbtwn2  28993  axeuclidlem  29050  axcontlem9  29060  axcontlem10  29061  umgrvad2edg  29301  upgrwlkdvdelem  29824  usgr2wlkneq  29844  2wlkdlem6  30019  umgr2adedgwlklem  30032  umgr2adedgspth  30036  2pthfrgrrn2  30373  frgrnbnb  30383  fusgr2wsp2nb  30424  nmcvcn  30786  sspmval  30824  sspimsval  30829  shsubcl  31311  shorth  31386  5oalem6  31750  strlem1  32341  atexch  32472  cdj3i  32532  xrofsup  32860  nnindf  32913  cnre2csqima  34076  nummin  35257  subgrwlk  35335  cusgr3cyclex  35339  erdszelem9  35402  erdsze2lem2  35407  gonarlem  35597  satffunlem  35604  satefvfmla1  35628  ss2mcls  35771  funpsstri  35969  dfon2lem4  35987  dfon2  35993  wsuclem  36026  elfuns  36116  btwnswapid  36220  ifscgr  36247  hilbert1.2  36358  elicc3  36520  tailfb  36580  dfttc4lem2  36732  bj-nnfand  37065  bj-gabss  37255  bj-imdirval3  37511  pibt2  37744  wl-mo3t  37912  ltflcei  37940  tan2h  37944  mblfinlem3  37991  fzmul  38073  metf1o  38087  ismtycnv  38134  ismtyres  38140  crngohomfo  38338  cossss  38847  funALTVss  39116  disjss  39163  hlhgt2  39846  hl2at  39862  2llnjN  40024  2lplnj  40077  linepsubN  40209  cdlemg33b0  41158  dvh3dim3N  41906  mapdh9a  42246  fltaccoprm  43084  iocinico  43655  clcnvlem  44065  ismnushort  44743  pm11.59  44833  f1cof1b  47522  afvres  47617  afv2res  47684  isuspgrim0lem  48366  isuspgrimlem  48368  grlimprclnbgrvtx  48472  ply1mulgsumlem1  48859  fldivexpfllog2  49038