Theorem anim12d 558

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  anim12ii 559  anim1d 560  anim2d 561  im2anan9 563  im2anan9r 564  pm5.74 583  pm5.18 660  3anim123d 900  hband 1111  hbbid 1112  2euswap 1445  exists2 1458  soss 2852  sotrieq 2861  wess 2936  ordtri3 2983  oneqmini 3017  ordunel 3084  weinxp 3233  xp11 3476  fun 3641  f1fv 3874  isotr 3897  isotrALT 3898  f1oweALT 3906  tfrlem1 3911  tz7.48lem 3955  om00 4206  omsmo 4257  ensdomtr 4471  domsdomtr 4476  aceq5 4740  zorn2lem6 4793  unidom 4808  alephord 4875  cardaleph 4885  indpi 5034  genpnmax 5110  reclem3pr 5158  reclem4pr 5159  suplem1pr 5161  suppsr2 5223  suppsr3 5224  pre-axsup 5291  xrre2t 5570  lemul12ait 5842  nnind 5937  lbreu 6045  xrsupexmnf 6074  xrinfmexpnf 6075  elnn0nn 6171  uzwo5OLD 6211  qbtwnre 6278  eliooordt 6388  elioc2t 6390  elico2t 6391  elicc2t 6392  uz11t 6432  sqrlem5 6677  replimt 6761  caubnd 6926  climaddlem3 7116  climmullem8 7127  caucvglem2 7158  rescncf 7272  infmap2lem2 7580  basgen2t 7639  opnin 7869  metcnss2 7899  cncfmet 7905  caussi 7954  iscms2lem4 7992  grplactf1o 8098  subgabl 8123  sspmval 8392  sspival 8397  sspimsval 8399  sspph 8515  pslem 8647  spwpr3OLD 8662  spwpr4OLD 8663  spwpr4aOLD 8664  shsubclt 9089  shsubcltOLD 9090  shorth 9168  occllem7 9179  projlem27 9212  osumlem4 9581  5oalem6 9604  strlem1 10177  atexcht 10308  cdj3 10368  uninqs 10441  oooeqim2 10476  cnrsfin 10509  cnrscoa 10510  cmphmp 10521  homcard 10539  filintf 10569  trnij 10637  ismonc 10742

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain