Theorem anim12d 333

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 293	1 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anim1d  334  anim2d  335  anim12  342  im2anan9  593  anim12dan  595  3anim123d  1314  hband  1482  hbbid  1568  spsbim  1836  moim  2083  moimv  2085  2euswapdc  2110  rspcimedv  2836  soss  4299  trin2  5002  xp11m  5049  funss  5217  fun  5370  dff13  5747  f1eqcocnv  5770  isores3  5794  isosolem  5803  f1o2ndf1  6207  tposfn2  6245  tposf1o2  6249  nndifsnid  6486  nnaordex  6507  supmoti  6970  isotilem  6983  recexprlemss1l  7597  recexprlemss1u  7598  caucvgsrlemoffres  7762  suplocsrlem  7770  nnindnn  7855  eqord1  8402  lemul12b  8777  lt2msq  8802  lbreu  8861  cju  8877  nnind  8894  uz11  9509  xrre2  9778  ico0  10218  ioc0  10219  expcan  10650  gcdaddm  11939  bezoutlemaz  11958  bezoutlembz  11959  isprm3  12072  prmdiveq  12190  epttop  12884  cnptopresti  13032  cnptoprest  13033  txcnp  13065  addcncntoplem  13345  mulcncflem  13384  bj-stand  13783  exmidsbthrlem  14054