Theorem imp31 362

Description: An importation inference.

Hypothesis

Ref	Expression
imp3.1	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
imp31	|- (((ph /\ ps) /\ ch) -> th)

Proof of Theorem imp31

Step	Hyp	Ref	Expression
1		imp3.1	. . 3 |- (ph -> (ps -> (ch -> th)))
2	1	imp 350	. 2 |- ((ph /\ ps) -> (ch -> th))
3	2	imp 350	1 |- (((ph /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  imp41 368  anassrs 441  ancom1s 489  ancom31s 490  3imp 825  3expa 831  pwssun 2816  fri 2908  ordelord 2960  tz7.7 2963  onint 2996  limsssuc 3111  findsg 3147  tfindsg 3152  weinxp 3223  dfimafn 3746  funimass4 3748  funimass3 3791  isomin 3884  tfrlem1 3896  tfrlem9 3904  elrnoprabg 4108  oecl 4156  oaordi 4164  oaass 4179  omordi 4181  odi 4194  oen0 4197  oeordi 4198  oeworde 4204  oaabs 4236  omsmolem 4240  sdomen2 4462  xpmapenlem4 4479  php3 4495  unblem1 4517  r1ord 4627  rankr1 4646  aceq5 4712  zorn2lem7 4766  unidom 4780  mulcanpi 4999  ltexprlem7 5120  reclem3pr 5130  suplem1pr 5133  suppsr2 5195  suppsr3 5196  supsr 5203  sup3 5999  elnnz 6092  qbtwnre 6216  ser1add2 6275  sqlecant 6572  cau4i 6855  cau5 6856  fsumsplit 6958  climsqueeze 7076  climsqueeze2 7077  isum1p 7141  unbenlem 7447  infpnlem1 7449  infxpidmlem12 7506  tgclt 7566  retopbas 7597  cnsscnp 7711  cncnplem2 7714  sncld 7726  mettri4 7753  metxplem4 7773  bl2in 7783  ssbl 7795  metcnpi3 7831  metcnpi4 7832  metcni2 7834  lmle 7895  bcthlem16 7948  bcthlem19 7951  bcthlem20 7952  bcthlem28 7960  grpidinvlem3 7984  ubthlem5 8464  ubthlem10 8469  ubthlem11 8470  minvecex 8509  pilem2 8591  projlem26 9127  projlem28 9129  osumlem6 9500  mdexch 10170  atoml 10217  mdsymlem5 10242  sumdmdlem 10252  uninqs 10342  infi1 10347  truni1 10386  cnvhmphb 10413  efilcp 10445  cnfilca 10451  cmpmon 10585  icmpmon 10587

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