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  1329  hband  1499  hbbid  1585  spsbim  1853  moim  2100  moimv  2102  2euswapdc  2127  rspcimedv  2855  soss  4326  trin2  5032  xp11m  5079  funss  5247  fun  5400  dff13  5782  f1eqcocnv  5805  isores3  5829  isosolem  5838  f1o2ndf1  6243  tposfn2  6281  tposf1o2  6285  nndifsnid  6522  nnaordex  6543  supmoti  7006  isotilem  7019  recexprlemss1l  7648  recexprlemss1u  7649  caucvgsrlemoffres  7813  suplocsrlem  7821  nnindnn  7906  eqord1  8454  lemul12b  8832  lt2msq  8857  lbreu  8916  cju  8932  nnind  8949  uz11  9564  xrre2  9835  ico0  10276  ioc0  10277  expcan  10710  gcdaddm  11999  bezoutlemaz  12018  bezoutlembz  12019  isprm3  12132  prmdiveq  12250  mulgpropdg  13057  imasabl  13171  subrgdvds  13455  epttop  13886  cnptopresti  14034  cnptoprest  14035  txcnp  14067  addcncntoplem  14347  mulcncflem  14386  bj-stand  14796  exmidsbthrlem  15067