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  1330  hband  1500  hbbid  1586  spsbim  1854  moim  2106  moimv  2108  2euswapdc  2133  rspcimedv  2867  soss  4346  trin2  5058  xp11m  5105  funss  5274  fun  5427  dff13  5812  f1eqcocnv  5835  isores3  5859  isosolem  5868  f1o2ndf1  6283  tposfn2  6321  tposf1o2  6325  nndifsnid  6562  nnaordex  6583  supmoti  7054  isotilem  7067  recexprlemss1l  7697  recexprlemss1u  7698  caucvgsrlemoffres  7862  suplocsrlem  7870  nnindnn  7955  eqord1  8504  lemul12b  8882  lt2msq  8907  lbreu  8966  cju  8982  nnind  9000  uz11  9618  xrre2  9890  ico0  10333  ioc0  10334  expcan  10790  gcdaddm  12124  bezoutlemaz  12143  bezoutlembz  12144  isprm3  12259  prmdiveq  12377  mulgpropdg  13237  imasabl  13409  subrgdvds  13734  epttop  14269  cnptopresti  14417  cnptoprest  14418  txcnp  14450  addcncntoplem  14740  mulcncflem  14786  bj-stand  15310  exmidsbthrlem  15582