Theorem anim12d 585

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 500	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 197  df-an 386

This theorem is referenced by:  anim12d1  586  anim1d  587  anim2d  588  prth  594  im2anan9  879  anim12dan  881  3anim123d  1403  mo3  2506  2euswap  2547  ssunsn2  4334  disjiun  4613  soss  5023  wess  5071  frinxp  5155  trin2  5488  xp11  5538  ordtri3OLD  5729  oneqmini  5745  funss  5876  fun  6033  fvcofneq  6333  dff13  6477  f1cofveqaeq  6480  f1eqcocnv  6521  isores3  6550  isosolem  6562  isowe2  6565  ordom  7036  f1oweALT  7112  f1o2ndf1  7245  tposfn2  7334  tposf1o2  7338  wfrlem4  7378  smo11  7421  tz7.48lem  7496  om00  7615  omsmo  7694  ixpfi2  8224  elfiun  8296  supmo  8318  infmo  8361  alephord  8858  cardaleph  8872  dfac5  8911  fin1a2lem9  9190  axdc3lem2  9233  zorn2lem6  9283  grudomon  9599  indpi  9689  genpnmax  9789  reclem3pr  9831  reclem4pr  9832  suplem1pr  9834  supsrlem  9892  dedekind  10160  lemul12b  10840  fimaxre  10928  lbreu  10933  supadd  10951  supmullem2  10954  cju  10976  nnind  10998  uz11  11670  xrre2  11960  qbtwnre  11989  xrsupexmnf  12094  xrinfmexpnf  12095  ico0  12179  ioc0  12180  ssfzoulel  12519  ishashinf  13201  swrdccatin2  13440  coss12d  13661  sqrlem6  13938  o1lo1  14218  ruclem9  14911  isprm3  15339  eulerthlem2  15430  prmdiveq  15434  ramub2  15661  cictr  16405  joinfval  16941  meetfval  16955  clatl  17056  lubun  17063  ipodrsima  17105  dirtr  17176  mulgpropd  17524  dprdss  18368  subrgdvds  18734  dmatsubcl  20244  scmatcrng  20267  epttop  20753  cnpresti  21032  cnprest  21033  lmmo  21124  1stcrest  21196  lly1stc  21239  txcnp  21363  addcnlem  22607  clmvscom  22830  caussi  23035  bcthlem5  23065  ovollb2lem  23196  voliunlem1  23258  ioombl1lem4  23269  rolle  23691  c1lip1  23698  c1lip3  23700  ulmval  24072  sqf11  24799  fsumvma  24872  dchrelbas3  24897  acopy  25658  brbtwn2  25719  axeuclidlem  25776  axcontlem9  25786  axcontlem10  25787  umgrvad2edg  26032  upgrwlkdvdelem  26535  usgr2wlkneq  26555  2wlkdlem6  26730  umgr2adedgwlklem  26743  umgr2adedgspth  26747  2pthfrgrrn2  27045  frgrnbnb  27055  frgr2wwlkeqm  27088  fusgr2wsp2nb  27090  nmcvcn  27438  sspmval  27476  sspimsval  27481  sspph  27598  shsubcl  27965  shorth  28042  5oalem6  28406  strlem1  28997  atexch  29128  cdj3i  29188  xrofsup  29418  nnindf  29448  cnre2csqima  29781  erdszelem9  30942  erdsze2lem2  30947  ss2mcls  31226  funpsstri  31420  dfon2lem4  31445  dfon2  31451  trpredrec  31492  frmin  31493  wsuclem  31527  wsuclemOLD  31528  frrlem4  31537  nocvxminlem  31606  nocvxmin  31607  elfuns  31717  btwnswapid  31819  ifscgr  31846  hilbert1.2  31957  elicc3  32006  tailfb  32067  wl-mo3t  33029  ltflcei  33068  tan2h  33072  mblfinlem3  33119  fzmul  33208  metf1o  33222  ismtycnv  33272  ismtyres  33278  crngohomfo  33476  hlhgt2  34194  hl2at  34210  2llnjN  34372  2lplnj  34425  linepsubN  34557  cdlemg33b0  35508  dvh3dim3N  36257  mapdh9a  36598  iocinico  37317  clcnvlem  37450  pm11.59  38112  afvres  40586  rhmsscrnghm  41344  ply1mulgsumlem1  41492  fldivexpfllog2  41681