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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anim1d  336  anim2d  337  anim12  344  im2anan9  606  anim12dan  608  3anim123d  1360  hband  1542  hbbid  1628  spsbim  1896  moim  2151  moimv  2153  2euswapdc  2178  rspcimedv  2931  soss  4459  trin2  5179  xp11m  5226  funss  5396  fun  5561  dff13  5974  f1eqcocnv  5997  isores3  6021  isosolem  6030  f1o2ndf1  6464  tposfn2  6537  tposf1o2  6541  nndifsnid  6780  nnaordex  6801  supmoti  7333  isotilem  7346  recexprlemss1l  8002  recexprlemss1u  8003  caucvgsrlemoffres  8167  suplocsrlem  8175  nnindnn  8260  eqord1  8812  lemul12b  9193  lt2msq  9218  lbreu  9277  cju  9293  nnind  9322  uz11  9954  xrre2  10233  ico0  10706  ioc0  10707  expcan  11168  swrdccatin2  11515  gcdaddm  12777  bezoutlemaz  12796  bezoutlembz  12797  isprm3  12912  prmdiveq  13034  mulgpropdg  14016  imasabl  14189  subrgdvds  14592  epttop  15240  cnptopresti  15388  cnptoprest  15389  txcnp  15421  addcncntoplem  15711  mulcncflem  15757  umgrvad2edg  16550  wlk1walkdom  16698  bj-stand  16874  exmidsbthrlem  17165