Theorem anim12d 586

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  587  anim1d  588  anim2d  589  prth  595  im2anan9  880  anim12dan  882  3anim123d  1406  mo3  2507  2euswap  2548  ssunsn2  4359  disjiun  4640  soss  5053  wess  5101  frinxp  5184  trin2  5519  xp11  5569  ordtri3OLD  5760  oneqmini  5776  funss  5907  fun  6066  fvcofneq  6367  dff13  6512  f1cofveqaeq  6515  f1eqcocnv  6556  isores3  6585  isosolem  6597  isowe2  6600  ordom  7074  f1oweALT  7152  f1o2ndf1  7285  tposfn2  7374  tposf1o2  7378  wfrlem4  7418  smo11  7461  tz7.48lem  7536  om00  7655  omsmo  7734  ixpfi2  8264  elfiun  8336  supmo  8358  infmo  8401  alephord  8898  cardaleph  8912  dfac5  8951  fin1a2lem9  9230  axdc3lem2  9273  zorn2lem6  9323  grudomon  9639  indpi  9729  genpnmax  9829  reclem3pr  9871  reclem4pr  9872  suplem1pr  9874  supsrlem  9932  dedekind  10200  lemul12b  10880  fimaxre  10968  lbreu  10973  supadd  10991  supmullem2  10994  cju  11016  nnind  11038  uz11  11710  xrre2  12001  qbtwnre  12030  xrsupexmnf  12135  xrinfmexpnf  12136  ico0  12221  ioc0  12222  ssfzoulel  12562  ishashinf  13247  swrdccatin2  13487  coss12d  13711  sqrlem6  13988  o1lo1  14268  ruclem9  14967  isprm3  15396  eulerthlem2  15487  prmdiveq  15491  ramub2  15718  cictr  16465  joinfval  17001  meetfval  17015  clatl  17116  lubun  17123  ipodrsima  17165  dirtr  17236  mulgpropd  17584  dprdss  18428  subrgdvds  18794  dmatsubcl  20304  scmatcrng  20327  epttop  20813  cnpresti  21092  cnprest  21093  lmmo  21184  1stcrest  21256  lly1stc  21299  txcnp  21423  addcnlem  22667  clmvscom  22890  caussi  23095  bcthlem5  23125  ovollb2lem  23256  voliunlem1  23318  ioombl1lem4  23329  rolle  23753  c1lip1  23760  c1lip3  23762  ulmval  24134  sqf11  24865  fsumvma  24938  dchrelbas3  24963  acopy  25724  brbtwn2  25785  axeuclidlem  25842  axcontlem9  25852  axcontlem10  25853  umgrvad2edg  26105  upgrwlkdvdelem  26632  usgr2wlkneq  26652  2wlkdlem6  26827  umgr2adedgwlklem  26840  umgr2adedgspth  26844  2pthfrgrrn2  27147  frgrnbnb  27157  fusgr2wsp2nb  27198  nmcvcn  27550  sspmval  27588  sspimsval  27593  sspph  27710  shsubcl  28077  shorth  28154  5oalem6  28518  strlem1  29109  atexch  29240  cdj3i  29300  xrofsup  29533  nnindf  29565  cnre2csqima  29957  erdszelem9  31181  erdsze2lem2  31186  ss2mcls  31465  funpsstri  31663  dfon2lem4  31691  dfon2  31697  trpredrec  31738  frmin  31739  wsuclem  31773  wsuclemOLD  31774  frrlem4  31783  nocvxminlem  31893  nocvxmin  31894  conway  31910  elfuns  32022  btwnswapid  32124  ifscgr  32151  hilbert1.2  32262  elicc3  32311  tailfb  32372  wl-mo3t  33358  ltflcei  33397  tan2h  33401  mblfinlem3  33448  fzmul  33537  metf1o  33551  ismtycnv  33601  ismtyres  33607  crngohomfo  33805  hlhgt2  34675  hl2at  34691  2llnjN  34853  2lplnj  34906  linepsubN  35038  cdlemg33b0  35989  dvh3dim3N  36738  mapdh9a  37079  iocinico  37797  clcnvlem  37930  pm11.59  38591  afvres  41252  rhmsscrnghm  42026  ply1mulgsumlem1  42174  fldivexpfllog2  42359