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  1331  hband  1511  hbbid  1597  spsbim  1865  moim  2117  moimv  2119  2euswapdc  2144  rspcimedv  2878  soss  4359  trin2  5071  xp11m  5118  funss  5287  fun  5442  dff13  5827  f1eqcocnv  5850  isores3  5874  isosolem  5883  f1o2ndf1  6304  tposfn2  6342  tposf1o2  6346  nndifsnid  6583  nnaordex  6604  supmoti  7077  isotilem  7090  recexprlemss1l  7730  recexprlemss1u  7731  caucvgsrlemoffres  7895  suplocsrlem  7903  nnindnn  7988  eqord1  8538  lemul12b  8916  lt2msq  8941  lbreu  9000  cju  9016  nnind  9034  uz11  9653  xrre2  9925  ico0  10385  ioc0  10386  expcan  10842  gcdaddm  12224  bezoutlemaz  12243  bezoutlembz  12244  isprm3  12359  prmdiveq  12477  mulgpropdg  13418  imasabl  13590  subrgdvds  13915  epttop  14480  cnptopresti  14628  cnptoprest  14629  txcnp  14661  addcncntoplem  14951  mulcncflem  14997  bj-stand  15548  exmidsbthrlem  15825