Theorem anim12d 557

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 555	. 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 558  anim1d 559  anim2d 560  im2anan9 562  im2anan9r 563  pm5.74 582  pm5.18 659  3anim123d 899  hband 1110  hbbid 1111  2euswap 1444  exists2 1457  soss 2848  sotrieq 2857  wess 2932  ordtri3 2979  oneqmini 3013  ordunel 3080  weinxp 3229  xp11 3472  fun 3636  f1fv 3869  isotr 3892  isotrALT 3893  f1oweALT 3901  tfrlem1 3906  tz7.48lem 3950  om00 4199  omsmo 4250  ensdomtr 4460  domsdomtr 4465  aceq5 4723  zorn2lem6 4776  unidom 4791  alephord 4858  cardaleph 4868  indpi 5017  genpnmax 5093  reclem3pr 5141  reclem4pr 5142  suplem1pr 5144  suppsr2 5206  suppsr3 5207  pre-axsup 5274  xrre2t 5553  lemul12ait 5808  nnind 5895  lbreu 6002  xrsupexmnf 6031  xrinfmexpnf 6032  elnn0nn 6128  uzwo5OLD 6169  qbtwnre 6228  elioc2t 6335  elico2t 6336  elicc2t 6337  ioossicc 6343  uz11t 6377  sqrlem5 6622  replimt 6707  caubnd 6878  climaddlem3 7069  climmullem8 7080  caucvglem2 7111  rescncf 7224  infmap2lem2 7540  basgen2t 7599  opnin 7831  metcnss2 7861  cncfmet 7867  caussi 7916  iscms2lem4 7954  grplactf1o 8061  subgabl 8087  sspmval 8354  sspival 8359  sspimsval 8361  sspph 8474  pslem 8605  shsubclt 9044  shsubcltOLD 9045  shorth 9123  occllem7 9134  projlem27 9167  osumlem4 9538  5oalem6 9561  strlem1 10133  atexcht 10264  cdj3 10324  gelsupvalOLD 10376  uninqs 10400  oooeqim2 10429  cnrsfin 10455  cnrscoa 10456  cmphmp 10467  homcard 10485  filintf 10502  trnij 10553  ismonc 10656

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