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  5909  f1eqcocnv  5932  isores3  5956  isosolem  5965  f1o2ndf1  6393  tposfn2  6432  tposf1o2  6436  nndifsnid  6675  nnaordex  6696  supmoti  7192  isotilem  7205  recexprlemss1l  7855  recexprlemss1u  7856  caucvgsrlemoffres  8020  suplocsrlem  8028  nnindnn  8113  eqord1  8663  lemul12b  9041  lt2msq  9066  lbreu  9125  cju  9141  nnind  9159  uz11  9779  xrre2  10056  ico0  10522  ioc0  10523  expcan  10979  swrdccatin2  11314  gcdaddm  12573  bezoutlemaz  12592  bezoutlembz  12593  isprm3  12708  prmdiveq  12826  mulgpropdg  13769  imasabl  13941  subrgdvds  14268  epttop  14833  cnptopresti  14981  cnptoprest  14982  txcnp  15014  addcncntoplem  15304  mulcncflem  15350  umgrvad2edg  16081  wlk1walkdom  16229  bj-stand  16395  exmidsbthrlem  16677