MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anim12d Structured version   Visualization version   GIF version

Theorem anim12d 609
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
StepHypRef Expression
1 anim12d.1 . 2 (𝜑 → (𝜓𝜒))
2 anim12d.2 . 2 (𝜑 → (𝜃𝜏))
3 idd 24 . 2 (𝜑 → ((𝜒𝜏) → (𝜒𝜏)))
41, 2, 3syl2and 608 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff setvar class
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 206  df-an 397
This theorem is referenced by:  anim12d1  610  anim1d  611  anim2d  612  anim12dan  619  3anim123d  1443  mo3  2562  mo4  2564  2euswapv  2630  2euswap  2645  disj  4405  ssunsn2  4785  prel12g  4819  disjiun  5090  soss  5563  wess  5618  frinxp  5712  trin2  6075  xp11  6125  oneqmini  6367  funss  6517  fvcofneq  7039  dff13  7198  f1cofveqaeq  7201  f1eqcocnv  7243  f1eqcocnvOLD  7244  isores3  7276  isosolem  7288  isowe2  7291  trom  7807  f1oweALT  7901  f1o2ndf1  8050  suppofssd  8130  tposfn2  8175  tposf1o2  8179  frrlem4  8216  wfrlem4OLD  8254  smo11  8306  tz7.48lem  8383  om00  8518  omsmo  8600  ixpfi2  9290  elfiun  9362  supmo  9384  infmo  9427  frmin  9681  cardaleph  10021  dfac5  10060  fin1a2lem9  10340  axdc3lem2  10383  zorn2lem6  10433  indpi  10839  genpnmax  10939  reclem3pr  10981  reclem4pr  10982  suplem1pr  10984  supsrlem  11043  dedekind  11314  lemul12b  12008  lbreu  12101  supadd  12119  supmullem2  12122  cju  12145  nnind  12167  uz11  12784  xrre2  13081  qbtwnre  13110  ico0  13302  ioc0  13303  ssfzoulel  13658  ishashinf  14354  swrdccatin2  14609  coss12d  14849  01sqrexlem6  15124  o1lo1  15411  ruclem9  16112  isprm3  16551  eulerthlem2  16646  prmdiveq  16650  ramub2  16878  cictr  17680  clatl  18389  lubun  18396  ipodrsima  18422  dirtr  18483  smndex1mgm  18709  smndex1sgrp  18710  smndex1mnd  18712  mulgpropd  18909  dprdss  19799  subrgdvds  20221  dmatsubcl  21831  scmatcrng  21854  epttop  22343  cnprest  22624  lmmo  22715  lly1stc  22831  txcnp  22955  addcnlem  24211  clmvscom  24437  caussi  24645  bcthlem5  24676  ovollb2lem  24836  voliunlem1  24898  ioombl1lem4  24909  rolle  25338  c1lip1  25345  c1lip3  25347  ulmval  25723  sqf11  26472  fsumvma  26545  dchrelbas3  26570  nocvxminlem  27101  nocvxmin  27102  conway  27122  cofcut1  27223  acopy  27661  brbtwn2  27740  axeuclidlem  27797  axcontlem9  27807  axcontlem10  27808  umgrvad2edg  28047  upgrwlkdvdelem  28570  usgr2wlkneq  28590  2wlkdlem6  28762  umgr2adedgwlklem  28775  umgr2adedgspth  28779  2pthfrgrrn2  29113  frgrnbnb  29123  fusgr2wsp2nb  29164  nmcvcn  29523  sspmval  29561  sspimsval  29566  shsubcl  30048  shorth  30123  5oalem6  30487  strlem1  31078  atexch  31209  cdj3i  31269  xrofsup  31555  nnindf  31598  cnre2csqima  32361  nummin  33564  subgrwlk  33595  cusgr3cyclex  33599  erdszelem9  33662  erdsze2lem2  33667  gonarlem  33857  satffunlem  33864  satefvfmla1  33888  ss2mcls  34031  funpsstri  34210  dfon2lem4  34231  dfon2  34237  wsuclem  34270  elfuns  34467  btwnswapid  34569  ifscgr  34596  hilbert1.2  34707  elicc3  34756  tailfb  34816  bj-nnfand  35181  bj-gabss  35372  bj-imdirval3  35622  pibt2  35855  wl-mo3t  35998  ltflcei  36033  tan2h  36037  mblfinlem3  36084  fzmul  36167  metf1o  36181  ismtycnv  36228  ismtyres  36234  crngohomfo  36432  cossss  36854  funALTVss  37128  disjss  37160  hlhgt2  37819  hl2at  37835  2llnjN  37997  2lplnj  38050  linepsubN  38182  cdlemg33b0  39131  dvh3dim3N  39879  mapdh9a  40219  fltaccoprm  40916  iocinico  41484  clcnvlem  41837  ismnushort  42523  pm11.59  42613  f1cof1b  45241  afvres  45336  afv2res  45403  isomuspgrlem1  45951  isomuspgrlem2c  45954  isomuspgrlem2d  45955  rhmsscrnghm  46256  ply1mulgsumlem1  46399  fldivexpfllog2  46583
  Copyright terms: Public domain W3C validator