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  600  anim12dan  602  3anim123d  1353  hband  1535  hbbid  1621  spsbim  1889  moim  2142  moimv  2144  2euswapdc  2169  rspcimedv  2909  soss  4405  trin2  5120  xp11m  5167  funss  5337  fun  5499  dff13  5898  f1eqcocnv  5921  isores3  5945  isosolem  5954  f1o2ndf1  6380  tposfn2  6418  tposf1o2  6422  nndifsnid  6661  nnaordex  6682  supmoti  7171  isotilem  7184  recexprlemss1l  7833  recexprlemss1u  7834  caucvgsrlemoffres  7998  suplocsrlem  8006  nnindnn  8091  eqord1  8641  lemul12b  9019  lt2msq  9044  lbreu  9103  cju  9119  nnind  9137  uz11  9757  xrre2  10029  ico0  10493  ioc0  10494  expcan  10950  swrdccatin2  11276  gcdaddm  12520  bezoutlemaz  12539  bezoutlembz  12540  isprm3  12655  prmdiveq  12773  mulgpropdg  13716  imasabl  13888  subrgdvds  14214  epttop  14779  cnptopresti  14927  cnptoprest  14928  txcnp  14960  addcncntoplem  15250  mulcncflem  15296  umgrvad2edg  16024  wlk1walkdom  16100  bj-stand  16167  exmidsbthrlem  16450