Theorem anim12d 569

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

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  anim12ii 570  anim1d 571  anim2d 572  im2anan9 574  im2anan9r 575  pm5.74 594  pm5.18 671  3anim123d 912  hband 1152  hbbid 1153  2euswap 1488  exists2 1503  soss 2908  sotrieq 2917  wess 2993  ordtri3 3040  oneqmini 3074  ordunel 3141  weinxp 3290  xp11 3533  fun 3698  f1fv 3931  isotr 3955  isotrALT 3956  f1oweALT 3964  tfrlem1 3969  tz7.48lem 4013  om00 4264  omsmo 4315  ensdomtr 4534  domsdomtr 4539  aceq5 4802  zorn2lem6 4855  unidom 4870  alephord 4940  cardaleph 4950  indpi 5099  genpnmax 5175  reclem3pr 5223  reclem4pr 5224  suplem1pr 5226  suppsr2 5288  suppsr3 5289  pre-axsup 5356  xrre2 5635  lemul12b 5900  nnind 5997  lbreu 6127  xrsupexmnf 6156  xrinfmexpnf 6157  elnn0nn 6253  uzwo5OLD 6296  qbtwnre 6331  eliooord 6413  elioc2 6415  elico2 6416  elicc2 6417  uz11 6458  sqrlem5 6767  replim 6851  caubndi 7016  climaddlem3 7206  climmullem8 7217  caucvglem2 7248  rescncf 7362  infmap2lem2 7672  basgen2 7728  opnin 7954  metcnss2 7984  cncfmet 7990  caussi 8039  iscms2lem4 8077  grplactf1o 8182  subgabl 8207  sspmval 8476  sspival 8481  sspimsval 8483  sspph 8599  pslem 8731  spwpr4OLD 8746  spwpr4aOLD 8747  shsubcl 9172  shsubclOLD 9173  shorth 9251  occllem7 9262  projlem27 9295  osumlem4 9664  5oalem6 9687  strlem1 10261  atexch 10392  cdj3i 10452  uninqs 10527  oooeqim2 10556  cnrsfin 10603  cnrscoa 10604  cmphmp 10615  homcard 10633  filintf 10662  trnij 10719  ismonc 10824  iepiclem 10833  isepic 10834

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 154  df-an 232

Copyright terms: Public domain