Theorem anim12d 561

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

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  anim12ii 562  anim1d 563  anim2d 564  im2anan9 566  im2anan9r 567  pm5.74 586  pm5.18 663  3anim123d 906  hband 1147  hbbid 1148  2euswap 1485  exists2 1499  soss 2931  sotrieq 2940  wess 2963  ordtri3 3011  oneqmini 3024  ordunel 3181  weinxp 3319  xp11 3561  fun 3748  dff13 3988  isotr 4011  isotrALT 4012  f1oweALT 4020  tfrlem1 4212  tz7.48lem 4256  om00 4342  omsmo 4397  ensdomtr 4616  domsdomtr 4621  xpfi 4685  aceq5 4886  zorn2lem6 4939  unidom 4954  alephord 5025  cardaleph 5035  indpi 5188  genpnmax 5264  reclem3pr 5312  reclem4pr 5313  suplem1pr 5315  suppsr2 5377  suppsr3 5378  pre-axsup 5445  xrre2 5724  lemul12b 5986  nnind 6082  lbreu 6213  xrsupexmnf 6242  xrinfmexpnf 6243  elnn0nn 6339  uzwo5OLD 6382  qbtwnre 6418  eliooord 6514  elioc2 6516  elico2 6517  elicc2 6518  uz11 6559  fzen 6622  sqrlem5 6878  replim 6962  caubndi 7129  climaddlem3 7319  climmullem8 7330  caucvglem2 7361  rescncf 7477  infmap2lem2 7792  basgen2 7851  opnin 8079  metcnss2 8110  cncfmet 8116  caussi 8165  iscms2lem4 8203  grplactf1o 8339  subgabl 8365  sspmval 8646  sspival 8651  sspimsval 8653  sspph 8771  pslem 8909  spwpr4 8925  spwpr4OLD 8926  spwpr4aOLD 8927  shsubcl 9365  shsubclOLD 9366  shorth 9444  occllem7 9455  projlem27 9488  osumlem4 9859  5oalem6 9882  strlem1 10458  atexch 10590  cdj3i 10650  uninqs 10730  oooeqim2 10759  inttr 10787  on1el3 10962  cnrsfin 11012  cnrscoa 11013  cmphmp 11027  homcard 11045  filintf 11081  trnij 11160  ismonc 11269  iepiclem 11278  isepic 11279  elicc3 11410  infenomsub 11450  locfincomp 11575  locfincf 11577  comppfsc 11578  topmtcl 11586  fgss 11634  limfilcf 11683  hausfillim 11685  tailfb 11762  fimax 11837  fimaxre 11856  sdclem2 11876  sdc 11877  metf1o 11907  mettrifi 11912  geomcau 11914  haustlmu 11967  uptx 11978  txcn 11979  txcnopab 11980  ismtycnv 12005  ismtyhmeo 12007  ismtybndlem 12008  ismtyres 12010  heiborlem1 12011  heiborlem32 12042  phtpyco 12098

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 145  df-an 223

Copyright terms: Public domain