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  602  anim12dan  604  3anim123d  1355  hband  1537  hbbid  1623  spsbim  1891  moim  2144  moimv  2146  2euswapdc  2171  rspcimedv  2912  soss  4411  trin2  5128  xp11m  5175  funss  5345  fun  5508  dff13  5908  f1eqcocnv  5931  isores3  5955  isosolem  5964  f1o2ndf1  6392  tposfn2  6431  tposf1o2  6435  nndifsnid  6674  nnaordex  6695  supmoti  7191  isotilem  7204  recexprlemss1l  7854  recexprlemss1u  7855  caucvgsrlemoffres  8019  suplocsrlem  8027  nnindnn  8112  eqord1  8662  lemul12b  9040  lt2msq  9065  lbreu  9124  cju  9140  nnind  9158  uz11  9778  xrre2  10055  ico0  10520  ioc0  10521  expcan  10977  swrdccatin2  11309  gcdaddm  12554  bezoutlemaz  12573  bezoutlembz  12574  isprm3  12689  prmdiveq  12807  mulgpropdg  13750  imasabl  13922  subrgdvds  14248  epttop  14813  cnptopresti  14961  cnptoprest  14962  txcnp  14994  addcncntoplem  15284  mulcncflem  15330  umgrvad2edg  16061  wlk1walkdom  16209  bj-stand  16344  exmidsbthrlem  16626