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  1503  hbbid  1589  spsbim  1857  moim  2109  moimv  2111  2euswapdc  2136  rspcimedv  2870  soss  4350  trin2  5062  xp11m  5109  funss  5278  fun  5433  dff13  5818  f1eqcocnv  5841  isores3  5865  isosolem  5874  f1o2ndf1  6295  tposfn2  6333  tposf1o2  6337  nndifsnid  6574  nnaordex  6595  supmoti  7068  isotilem  7081  recexprlemss1l  7721  recexprlemss1u  7722  caucvgsrlemoffres  7886  suplocsrlem  7894  nnindnn  7979  eqord1  8529  lemul12b  8907  lt2msq  8932  lbreu  8991  cju  9007  nnind  9025  uz11  9643  xrre2  9915  ico0  10370  ioc0  10371  expcan  10827  gcdaddm  12178  bezoutlemaz  12197  bezoutlembz  12198  isprm3  12313  prmdiveq  12431  mulgpropdg  13372  imasabl  13544  subrgdvds  13869  epttop  14434  cnptopresti  14582  cnptoprest  14583  txcnp  14615  addcncntoplem  14905  mulcncflem  14951  bj-stand  15502  exmidsbthrlem  15779