Theorem anim12d 335

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	|- ( ph -> ( ps -> ch ) )
anim12d.2	|- ( ph -> ( th -> ta ) )

Assertion

Ref	Expression
anim12d	|- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )

Proof of Theorem anim12d

Step	Hyp	Ref	Expression
1		anim12d.1	. 2 |- ( ph -> ( ps -> ch ) )
2		anim12d.2	. 2 |- ( ph -> ( th -> ta ) )
3		idd 21	. 2 |- ( ph -> ( ( ch /\ ta ) -> ( ch /\ ta ) ) )
4	1, 2, 3	syl2and 295	1 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anim1d  336  anim2d  337  anim12  344  im2anan9  598  anim12dan  600  3anim123d  1319  hband  1489  hbbid  1575  spsbim  1843  moim  2090  moimv  2092  2euswapdc  2117  rspcimedv  2843  soss  4314  trin2  5020  xp11m  5067  funss  5235  fun  5388  dff13  5768  f1eqcocnv  5791  isores3  5815  isosolem  5824  f1o2ndf1  6228  tposfn2  6266  tposf1o2  6270  nndifsnid  6507  nnaordex  6528  supmoti  6991  isotilem  7004  recexprlemss1l  7633  recexprlemss1u  7634  caucvgsrlemoffres  7798  suplocsrlem  7806  nnindnn  7891  eqord1  8439  lemul12b  8817  lt2msq  8842  lbreu  8901  cju  8917  nnind  8934  uz11  9549  xrre2  9820  ico0  10261  ioc0  10262  expcan  10695  gcdaddm  11984  bezoutlemaz  12003  bezoutlembz  12004  isprm3  12117  prmdiveq  12235  mulgpropdg  13023  subrgdvds  13354  epttop  13560  cnptopresti  13708  cnptoprest  13709  txcnp  13741  addcncntoplem  14021  mulcncflem  14060  bj-stand  14470  exmidsbthrlem  14740