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  7719  recexprlemss1u  7720  caucvgsrlemoffres  7884  suplocsrlem  7892  nnindnn  7977  eqord1  8527  lemul12b  8905  lt2msq  8930  lbreu  8989  cju  9005  nnind  9023  uz11  9641  xrre2  9913  ico0  10368  ioc0  10369  expcan  10825  gcdaddm  12176  bezoutlemaz  12195  bezoutlembz  12196  isprm3  12311  prmdiveq  12429  mulgpropdg  13370  imasabl  13542  subrgdvds  13867  epttop  14410  cnptopresti  14558  cnptoprest  14559  txcnp  14591  addcncntoplem  14881  mulcncflem  14927  bj-stand  15478  exmidsbthrlem  15753