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  600  anim12dan  602  3anim123d  1353  hband  1535  hbbid  1621  spsbim  1889  moim  2142  moimv  2144  2euswapdc  2169  rspcimedv  2910  soss  4409  trin2  5126  xp11m  5173  funss  5343  fun  5505  dff13  5904  f1eqcocnv  5927  isores3  5951  isosolem  5960  f1o2ndf1  6388  tposfn2  6427  tposf1o2  6431  nndifsnid  6670  nnaordex  6691  supmoti  7183  isotilem  7196  recexprlemss1l  7845  recexprlemss1u  7846  caucvgsrlemoffres  8010  suplocsrlem  8018  nnindnn  8103  eqord1  8653  lemul12b  9031  lt2msq  9056  lbreu  9115  cju  9131  nnind  9149  uz11  9769  xrre2  10046  ico0  10511  ioc0  10512  expcan  10968  swrdccatin2  11300  gcdaddm  12545  bezoutlemaz  12564  bezoutlembz  12565  isprm3  12680  prmdiveq  12798  mulgpropdg  13741  imasabl  13913  subrgdvds  14239  epttop  14804  cnptopresti  14952  cnptoprest  14953  txcnp  14985  addcncntoplem  15275  mulcncflem  15321  umgrvad2edg  16050  wlk1walkdom  16156  bj-stand  16280  exmidsbthrlem  16562