Theorem anim12d 431

Description: Conjoin antecedents and consequents in a deduction.

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		prth 429	. 2 |- (((ps -> ch) /\ (th -> ta )) -> ((ps /\ th) -> (ch /\ ta )))
2		anim12d.1	. 2 |- (ph -> (ps -> ch))
3		anim12d.2	. 2 |- (ph -> (th -> ta ))
4	1, 2, 3	sylanc 361	1 |- (ph -> ((ps /\ th) -> (ch /\ ta )))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  anim1d 432  anim2d 433  im2anan9 434  im2anan9r 435  pm5.74 442  pm5.18 497  hband 788  hbbid 789  del43 856  2euswap 1065  exists2 1073  poss 2129  soss 2140  sotrieq 2149  wess 2188  ordtri3 2234  oneqmini 2272  weinxp 2467  fun 2763  f1fv 2916  isocnv 2934  isotr 2935  isotrALT 2936  f1oweOLD 2944  tfrlem1 2949  tz7.48lem 2993  tz7.49 2997  omsmo 3196  ensdomtr 3372  domsdomtr 3374  aceq5 3563  zornlem6 3608  alephord 3680  cardaleph 3690  indpi 3828  genpnmax 3904  reclem3pr 3952  reclem4pr 3953  suplem1pr 3955  suppsr2 4017  suppsr3 4018  axsup 4088  nnind 4434  elnn0nn 4593  uzwo2 4606  qbtwnre 4650  sqrlem5 4735  replimt 4798  infmap2lem2 4952  shsubclt 5125  shorth 5176  occllem7 5186  projlem27 5219  shintcl 5294  osumlem4 5533  5oalem6 5549  strlem1 5691  cvntrt 5724  atexch 5769

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org