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 490  ancom31s 491  3imp 826  3expa 832  moi2 1921  pwssun 2823  fri 2914  ordelord 2966  tz7.7 2969  onint 3002  limsssuc 3117  findsg 3153  tfindsg 3158  weinxp 3229  dfimafn 3756  funimass4 3758  funimass3 3801  isomin 3894  tfrlem1 3906  tfrlem9 3914  elrnoprabg 4117  oecl 4165  oaordi 4173  oaass 4188  omordi 4190  odi 4203  oen0 4206  oeordi 4207  oeworde 4213  oaabs 4245  omsmolem 4249  sdomen2 4471  xpmapenlem4 4488  php3 4504  unblem1 4526  r1ord 4638  rankr1 4657  aceq5 4723  zorn2lem7 4777  unidom 4791  mulcanpi 5010  ltexprlem7 5131  reclem3pr 5141  suplem1pr 5144  suppsr2 5206  suppsr3 5207  supsr 5214  sup3 6009  elnnz 6102  qbtwnre 6228  ser1add2 6288  sqlecant 6586  cau4i 6870  cau5 6871  fsumsplit 6973  climsqueeze 7093  climsqueeze2 7094  isum1p 7158  unbenlem 7464  infpnlem1 7466  infxpidmlem12 7523  tgclt 7584  retopbas 7615  cnsscnp 7732  cncnplem2 7735  sncld 7747  mettri4 7774  metxplem4 7795  bl2in 7805  ssbl 7817  metcnpi3 7854  metcnpi4 7855  metcni2 7857  lmle 7922  bcthlem16 7976  bcthlem19 7979  bcthlem20 7980  bcthlem28 7988  grpidinvlem3 8012  ubthlem5 8492  ubthlem10 8497  ubthlem11 8498  minvecex 8537  pilem2 8626  projlem26 9166  projlem28 9168  osumlem6 9540  mdexch 10218  atoml 10265  mdsymlem5 10290  sumdmdlem 10301  uninqs 10400  infi1 10405  truni1 10445  cnvhmphb 10472  efilcp 10504  cnfilca 10510  cmpmon 10657  icmpmon 10659

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